package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

Module `EConstr.EInstance`Source

Sourcetype t = Evd.einstance

Type of universe instances up-to universe unification. Similar to ESorts.t for UVars.Instance.t.

Sourceval make : UVars.Instance.t -> t

Sourceval kind : Evd.evar_map -> t -> UVars.Instance.t

Sourceval empty : t

Sourceval is_empty : t -> bool

Sourceval length : t -> int * int