Stream: Coq users

Topic: Transparent and Opaque inside Ltac

view this post on Zulip Natasha Klaus (Mar 25 2022 at 11:21):

Hello,

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).

view this post on Zulip Gaëtan Gilbert (Mar 25 2022 at 11:24):

https://coq.github.io/doc/master/refman/proofs/writing-proofs/equality.html#coq:tacn.with_strategy

view this post on Zulip Natasha Klaus (Mar 25 2022 at 11:33):

Thank you!

Last updated: Oct 03 2023 at 20:01 UTC