Fabian Kunze (Nov 24 2020 at 16:47): Fabian Kunze (Nov 24 2020 at 16:47):What is the Ltac2 equivalent of "let H := fresh in assert (H:=True))" ?
Pierre-Marie Pédrot (Nov 24 2020 at 16:47):There is a Fresh module
Pierre-Marie Pédrot (Nov 24 2020 at 16:49):so, something along the lines of let h := Fresh.of_goal @H in assert ($h := True)
Fabian Kunze (Nov 24 2020 at 16:50):oh, the version of the doc I saw did not have the "of_goal" function
Fabian Kunze (Nov 24 2020 at 16:50):thanks
Pierre-Marie Pédrot (Nov 24 2020 at 16:51):rather, Fresh.in_goal
Pierre-Marie Pédrot (Nov 24 2020 at 16:51):of_goal is part of Free, not Fresh, and generates a set of free variables
Fabian Kunze (Nov 24 2020 at 16:52):I reimplemented it by accident, as the stdlib-online doc did not show it :D let valt := Fresh.fresh (Fresh.Free.of_goal ()) @H in ...
Fabian Kunze (Nov 24 2020 at 16:53):No, it showed it, but i failed to readuntil the end
Pierre-Marie Pédrot (Nov 24 2020 at 16:53):We have an infrastructure problem with the Ltac2 documentation btw.
Pierre-Marie Pédrot (Nov 24 2020 at 16:54):The refman was designed to duplicate the information there, but it doesn't scale past a handful of primitive tactics.
Pierre-Marie Pédrot (Nov 24 2020 at 16:54):Since Ltac2 is a full-blown language, we should rely on coqdoc generated documentation for exploration.
Pierre-Marie Pédrot (Nov 24 2020 at 16:55):It's quite cumbersome to have to go reading the v file currently.
Fabian Kunze (Nov 24 2020 at 16:58):and can i tell ltac 2 that it should try to type my recursive function at unit? I think it tries to type it at constr, and now shows me the cases where unit is returned as errors. I'm not sure where the constr-idea comes from currently.
Pierre-Marie Pédrot (Nov 24 2020 at 17:00):Hard to tell without looking at the code.
Fabian Kunze (Nov 24 2020 at 17:16):Ah, no, i fail to find the translation for "lazymatch typeof H with ... end" in Ltac 2, that was the problem
Fabian Kunze (Nov 24 2020 at 17:16):and of course just using ltac1:() soes not work, as it is not a unit-tactic
Fabian Kunze (Nov 24 2020 at 17:17):Const.type :D
Last updated: Apr 16 2024 at 10:01 UTC