# Library Ltac2.Proj

Type of primitive projections. This includes the unfolding boolean.

Ltac2 @ external equal : t -> t -> bool := "coq-core.plugins.ltac2" "projection_equal".

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

Ltac2 @ external ind : t -> inductive := "coq-core.plugins.ltac2" "projection_ind".

Get the inductive to which the projectin belongs.

Ltac2 @ external index : t -> int := "coq-core.plugins.ltac2" "projection_index".

The index of the projection indicates which field it projects.

Ltac2 @ external unfolded : t -> bool := "coq-core.plugins.ltac2" "projection_unfolded".

Get the unfolding boolean.

Ltac2 @ external set_unfolded : t -> bool -> t

:= "coq-core.plugins.ltac2" "projection_set_unfolded".

Set the unfolding boolean.

Ltac2 @ external of_constant : constant -> t option

:= "coq-core.plugins.ltac2" "projection_of_constant".

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

Ltac2 @ external to_constant : t -> constant option

:= "coq-core.plugins.ltac2" "projection_to_constant".

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