Still learning things about Ltac2 so this may be a pretty naive question, but what is the Ltac2 equivalent of
refine ?["foo"], i.e. rename the current goal to some given string?
More Ltac2 questions (or maybe Coq questions?): Is it expected that this changes the number of goals from 1 to 0?
ltac1:(let n := numgoals in idtac "There are" n "goals"); assert ($h : True) by exact I; ltac1:(let n := numgoals in idtac "There are" n "goals");
There are 1 goals There are 0 goals
so where did my goal go?
Are you sure that in the second case, the "by" clause is only
exact I and not
exact I;ltac:(...)? (not sure about the precedence)
Ah, interesting! That might explain it. I also just found that
assert ($h := I);
does not have that problem…
Good catch, that was it. Tricky… Thanks! :-)
you could test
...;(refine _ by _);,,,
Right, that’s how I confirmed your theory
Or also place parens around (assert by).
Any tacticals that take a tactic have this bug, the tracker has an entry for the case of intuition.
They should take tactic3 instead.
Last updated: Feb 01 2023 at 11:04 UTC