Zoe Paraskevopoulou (Nov 14 2021 at 19:08): Zoe Paraskevopoulou (Nov 14 2021 at 19:08):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 .
Jason Gross (Nov 26 2021 at 01:45):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: Oct 12 2024 at 12:01 UTC