Joachim Breitner (Dec 05 2020 at 15:57): Joachim Breitner (Dec 05 2020 at 15:57):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?
Joachim Breitner (Dec 05 2020 at 16:59):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");
It prints:
There are 1 goals
There are 0 goals
so where did my goal go?
Fabian Kunze (Dec 05 2020 at 17:01):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)
Joachim Breitner (Dec 05 2020 at 17:03):Ah, interesting! That might explain it. I also just found that
assert ($h := I);
does not have that problem…
Joachim Breitner (Dec 05 2020 at 17:04):Good catch, that was it. Tricky… Thanks! :-)
Fabian Kunze (Dec 05 2020 at 17:04):you could test ...;(refine _ by _);,,,
Joachim Breitner (Dec 05 2020 at 17:06):Right, that’s how I confirmed your theory
Paolo Giarrusso (Dec 06 2020 at 01:32):Or also place parens around (assert by).
Paolo Giarrusso (Dec 06 2020 at 01:33):Any tacticals that take a tactic have this bug, the tracker has an entry for the case of intuition.
Paolo Giarrusso (Dec 06 2020 at 01:33):They should take tactic3 instead.
Last updated: Sep 26 2023 at 11:01 UTC