Stream: Coq users

Topic: Ltac 2 fresh

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: Oct 13 2024 at 01:02 UTC