diff options
| author | filliatr | 1999-10-13 12:20:02 +0000 |
|---|---|---|
| committer | filliatr | 1999-10-13 12:20:02 +0000 |
| commit | b5f6cce3f1aee416e5010a0a38f0508f107cd61e (patch) | |
| tree | 988e6723202430f73244f837c4f24767727da755 /kernel | |
| parent | eaddcc04b04512d9c60e7f832abdb1e13f2df6dc (diff) | |
documentation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@98 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/generic.mli | 23 |
1 files changed, 13 insertions, 10 deletions
diff --git a/kernel/generic.mli b/kernel/generic.mli index b9eb9a512d..49ec5bfbe5 100644 --- a/kernel/generic.mli +++ b/kernel/generic.mli @@ -7,18 +7,21 @@ open Names (*i*) (* \label{generic_terms} A generic notion of terms with binders, - over any kind of operators. *) + over any kind of operators. + [DLAM] is a de Bruijn binder on one term, and [DLAMV] on many terms. + [VAR] is used for named variables and [Rel] for variables as + de Bruijn indices. *) type 'oper term = - | DOP0 of 'oper (* atomic terms *) - | DOP1 of 'oper * 'oper term (* operator of arity 1 *) - | DOP2 of 'oper * 'oper term * 'oper term (* operator of arity 2 *) - | DOPN of 'oper * 'oper term array (* operator of variadic arity *) - | DOPL of 'oper * 'oper term list (* operator of variadic arity *) - | DLAM of name * 'oper term (* deBruijn binder on one term*) - | DLAMV of name * 'oper term array (* deBruijn binder on many terms*) - | VAR of identifier (* named variable *) - | Rel of int (* variable as deBruijn index *) + | DOP0 of 'oper + | DOP1 of 'oper * 'oper term + | DOP2 of 'oper * 'oper term * 'oper term + | DOPN of 'oper * 'oper term array + | DOPL of 'oper * 'oper term list + | DLAM of name * 'oper term + | DLAMV of name * 'oper term array + | VAR of identifier + | Rel of int val isRel : 'a term -> bool val isVAR : 'a term -> bool |