Hi all! Is there any way to find the number of the current goal in Ltac2? For example, I would like to be able do induction H; my_proof_script and be able to recover the goal number generated by the induction in the proof script .

Maybe you could create a reference, focus on a particular goal, and increment it in each goal? The equivalent of (pseudo-mix-of-ltac2-and-OCaml-and-ltac1) `let n := ref 0 in [ > (let goalnum := !n in n:=(!n+1); my_proof_script ) .. ]`

?

Last updated: May 18 2024 at 10:02 UTC