`TransparentState`#

Ltac2.TransparentState

type t = TransparentState.t

Type representing a transparency state. A transparency state is a set of variables, constants, and primitive projections.

val empty : t

empty is the empty transparency state (all constants are opaque).

val full : t

full is the full transparency state (all constants are transparent).

val current : unit -> t Proofview.tactic

current () gives the transparency state of the goal, which is influenced by, e.g., the Strategy command, or the with_strategy tactic.

val union : t -> t -> t

union t1 t2 builds a transparency state containing all the variables, constants, and primitive projections which are either in t1 or in t2.

val inter : t -> t -> t

inter t1 t2 builds a transparency state containing all the variables, constants, and primitive projections which are both in t1 and in t2.

val diff : t -> t -> t

diff t1 t2 builds a transparency state containing all the variables, constants, and primitive projections which are in t1 but not in t2.

val add_constant : constant -> t -> t

add_constant c t adds the constant c to the transparency state t. Does nothing if the constant is already present.

val add_proj : projection -> t -> t

add_proj p t adds the primitive projection p to the transparency state t. Does nothing if the projection is already present.

val add_var : ident -> t -> t

add_var v t adds the local variable v to the transparency state t. Does nothing if the variable is already present.

val remove_constant : constant -> t -> t

remove_constant c t removes the constant c from the transparency state t. Does nothing if the constant is not present.

val remove_proj : projection -> t -> t

remove_proj p t removes the primitive projection p from the transparency state t. Does nothing if the projection is not present.

val remove_var : ident -> t -> t

remove_var v t removes the local variable v from the transparency state t. Does nothing if the variable is not present.

val mem_constant : constant -> t -> bool

mem_constant c t checks whether the constant c is present in the transparency state t.

val mem_proj : projection -> t -> bool

mem_proj p t checks whether the primitive projection p is present in the transparency state t.

val mem_var : ident -> t -> bool

mem_var v t checks whether the local variable v is present in the transparency state t.

type strategy_level = private ..

Strategy levels used by with_strategy.

See Conv_oracle.level.

type strategy_level +=

| Expand
(*
Corresponds to the -oo level (always unfold).
*)
| Opaque
(*
Corresponds to the +oo level (never unfold).
*)
| Level of int
(*
Corresponds to integer level n (where Level 0 is transparent).
*)

val with_strategy :
  strategy_level ->
  reference list ->
  'a Proofview.tactic ->
  'a Proofview.tactic

with_strategy lvl refs tac temporarily sets the strategy level of all references in refs to lvl, executes tac, and then restores the original strategy levels. This is the Ltac2 analogue of the with_strategy Ltac tactic and the Strategy vernacular command.

since 9.3

TransparentState#

`TransparentState`#