Stream: Ltac2

Topic: Goal number


view this post on Zulip 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 .

view this post on Zulip 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: Jan 31 2023 at 10:01 UTC