Module Projection.ReprSource

Sourcetype t
Sourceval make : inductive -> proj_npars:int -> proj_arg:int -> Label.t -> t
include QNameS with type t := t
Sourcemodule CanOrd : EqType with type t = t

Equality functions over the canonical name. Their use should be restricted to the kernel.

Sourcemodule UserOrd : EqType with type t = t

Equality functions over the user name.

Sourcemodule SyntacticOrd : EqType with type t = t

Equality functions using both names, for low-level uses.

Sourceval constant : t -> Constant.t

Don't use this if you don't have to.

Sourceval inductive : t -> inductive
Sourceval mind : t -> MutInd.t
Sourceval npars : t -> int
Sourceval arg : t -> int
Sourceval label : t -> Label.t
Sourceval equal : t -> t -> bool
  • deprecated Use QProjection.equal
Sourceval hash : t -> int
  • deprecated Use QProjection.hash
Sourceval compare : t -> t -> int
  • deprecated Use QProjection.compare
Sourceval map : (MutInd.t -> MutInd.t) -> t -> t
Sourceval map_npars : (MutInd.t -> int -> MutInd.t * int) -> t -> t
Sourceval to_string : t -> string

Encode as a string (not to be used for user-facing messages).

Sourceval print : t -> Pp.t

Print internal representation (not to be used for user-facing messages).