I want to use tactic
make_tp inside proof. But receive error (The reference Transparent was not found in the current environment)
Definition number_10001 : Z.t := 10001. Opaque number_10001. Definition number_10000 : Z.t := 10000. Opaque number_10000. Ltac make_tp := Transparent number_10000; Transparent number_10001.
How can I do that? My problem is that I have several such
number definitions and I need to switch between them inside proof (make transparent / make opaque).
Last updated: Jan 29 2023 at 05:03 UTC