From e9caa75be87bdbd68d8ca2d7291f623bec6b93aa Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 13 Jun 2016 16:27:50 +0000 Subject: [PATCH] does_not_occur documented --- matita/components/ng_kernel/nCicTypeChecker.mli | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/matita/components/ng_kernel/nCicTypeChecker.mli b/matita/components/ng_kernel/nCicTypeChecker.mli index 6ca329fbf..34abacfde 100644 --- a/matita/components/ng_kernel/nCicTypeChecker.mli +++ b/matita/components/ng_kernel/nCicTypeChecker.mli @@ -64,6 +64,10 @@ val are_all_occurrences_positive: #NCic.status -> subst:NCic.substitution -> NCic.context -> NUri.uri -> int -> int -> int -> int -> NCic.term -> bool +(* does_not_occur ... n nn t + * detects the Rels m of t in the range n < m <= nn + * recursively delta-expanding the Rels m of t in the range 0 < m <= n + *) val does_not_occur : #NCic.status -> subst:NCic.substitution -> NCic.context -> int -> int -> NCic.term -> bool -- 2.39.2