diff options
Diffstat (limited to 'kernel/univ.mli')
| -rw-r--r-- | kernel/univ.mli | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/kernel/univ.mli b/kernel/univ.mli index 77ebf5a11..c45ebe21c 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -125,6 +125,13 @@ sig val for_all : (Level.t * int -> bool) -> t -> bool val map : (Level.t * int -> 'a) -> t -> 'a list + + (** [compact u] remaps local variables in [u] such that their indices become + consecutive. It returns the new universe and the mapping. + Example: compact [(Var 0, i); (Prop, 0); (Var 2; j))] = + [(Var 0,i); (Prop, 0); (Var 1; j)], [0; 2] + *) + val compact : t -> t * int list end type universe = Universe.t |