From 4fba4b00257e8ddbc94f71115d139bfc2483944d Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 27 Feb 2017 12:12:35 +0100 Subject: Expliciting and taking advantage of a representation invariant in Esubst. --- kernel/esubst.mli | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'kernel/esubst.mli') diff --git a/kernel/esubst.mli b/kernel/esubst.mli index b82d6fdf0..a674c425a 100644 --- a/kernel/esubst.mli +++ b/kernel/esubst.mli @@ -56,7 +56,11 @@ val comp : ('a subs * 'a -> 'a) -> 'a subs -> 'a subs -> 'a subs (** {6 Compact representation } *) (** Compact representation of explicit relocations - [ELSHFT(l,n)] == lift of [n], then apply [lift l]. - - [ELLFT(n,l)] == apply [l] to de Bruijn > [n] i.e under n binders. *) + - [ELLFT(n,l)] == apply [l] to de Bruijn > [n] i.e under n binders. + + Invariant ensured by the private flag: no lift contains two consecutive + [ELSHFT] nor two consecutive [ELLFT]. +*) type lift = private | ELID | ELSHFT of lift * int -- cgit v1.2.3