Proj

Ltac2.Proj

type t = projection

Type of primitive projections. This includes the unfolding boolean.

val equal : t -> t -> bool

equal p1 p2 tests equality of primitive projections.

Projections obtained through module aliases or Include are not considered equal by this function. The unfolding boolean is not ignored.

val ind : t -> inductive

ind proj returns the inductive to which the projection belongs.

val index : t -> int

index proj returns the index of the field that proj projects.

val unfolded : t -> bool

unfolded proj returns the unfolding boolean.

val set_unfolded : t -> bool -> t

set_unfolded proj unfolded sets the unfolding boolean.

val of_constant : constant -> t option

of_constant cst gets the primitive projection associated to the constant. The returned projection is folded. Returns None when the constant is not associated to a primitive projection.

val to_constant : t -> Names.Projection.Repr.t option

to_constant proj gets the constant associated to the primitive projection. Currently always returns Some but this may change in the future.

val print : t -> message

print proj prints the projection using the shortest qualified identifier which refers to it. Does not avoid variable names in the current or global environment.