diff options
Diffstat (limited to 'kernel/esubst.mli')
-rw-r--r-- | kernel/esubst.mli | 33 |
1 files changed, 18 insertions, 15 deletions
diff --git a/kernel/esubst.mli b/kernel/esubst.mli index bf1d23241..bbb3d838e 100644 --- a/kernel/esubst.mli +++ b/kernel/esubst.mli @@ -1,15 +1,16 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) +(*********************************************************************** + v * The Coq Proof Assistant / The Coq Development Team + <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud + \VV/ ************************************************************* + // * This file is distributed under the terms of the + * GNU Lesser General Public License Version 2.1 + ***********************************************************************) (*i $Id$ i*) -(*s Explicit substitutions of type ['a]. *) -(* - ESID(n) = %n END bounded identity +(** {6 Sect } *) +(** Explicit substitutions of type ['a]. + - ESID(n) = %n END bounded identity * - CONS([|t1..tn|],S) = (S.t1...tn) parallel substitution * (beware of the order: indice 1 is substituted by tn) * - SHIFT(n,S) = (^n o S) terms in S are relocated with n vars @@ -21,15 +22,16 @@ type 'a subs = | SHIFT of int * 'a subs | LIFT of int * 'a subs -(* Derived constructors granting basic invariants *) +(** Derived constructors granting basic invariants *) val subs_cons: 'a array * 'a subs -> 'a subs val subs_shft: int * 'a subs -> 'a subs val subs_lift: 'a subs -> 'a subs val subs_liftn: int -> 'a subs -> 'a subs -(* [subs_shift_cons(k,s,[|t1..tn|])] builds (^k s).t1..tn *) + +(** [subs_shift_cons(k,s,[|t1..tn|])] builds (^k s).t1..tn *) val subs_shift_cons: int * 'a subs * 'a array -> 'a subs -(* [expand_rel k subs] expands de Bruijn [k] in the explicit substitution +(** [expand_rel k subs] expands de Bruijn [k] in the explicit substitution * [subs]. The result is either (Inl(lams,v)) when the variable is * substituted by value [v] under lams binders (i.e. v *has* to be * shifted by lams), or (Inr (k',p)) when the variable k is just relocated @@ -38,17 +40,18 @@ val subs_shift_cons: int * 'a subs * 'a array -> 'a subs *) val expand_rel: int -> 'a subs -> (int * 'a, int * int option) Util.union -(* Tests whether a substitution behaves like the identity *) +(** Tests whether a substitution behaves like the identity *) val is_subs_id: 'a subs -> bool -(* Composition of substitutions: [comp mk_clos s1 s2] computes a +(** Composition of substitutions: [comp mk_clos s1 s2] computes a * substitution equivalent to applying s2 then s1. Argument * mk_clos is used when a closure has to be created, i.e. when * s1 is applied on an element of s2. *) val comp : ('a subs * 'a -> 'a) -> 'a subs -> 'a subs -> 'a subs -(*s Compact representation of explicit relocations. \\ +(** {6 Sect } *) +(** 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. *) type lift = |