From 21d58727027699d8617a7faab912843756b585ed Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 5 Jan 2005 14:07:33 +0000 Subject: [PATCH] exported lift_from --- helm/ocaml/cic_proof_checking/cicSubstitution.ml | 9 ++++++--- helm/ocaml/cic_proof_checking/cicSubstitution.mli | 4 ++++ 2 files changed, 10 insertions(+), 3 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.ml b/helm/ocaml/cic_proof_checking/cicSubstitution.ml index 38f2e7a6d..aff943757 100644 --- a/helm/ocaml/cic_proof_checking/cicSubstitution.ml +++ b/helm/ocaml/cic_proof_checking/cicSubstitution.ml @@ -30,7 +30,7 @@ exception ReferenceToConstant;; exception ReferenceToCurrentProof;; exception ReferenceToInductiveDefinition;; -let lift n = +let lift_from k n = let rec liftaux k = let module C = Cic in function @@ -95,10 +95,13 @@ let lift n = in C.CoFix (i, liftedfl) in + liftaux k + +let lift n t = if n = 0 then - (function t -> t) + t else - liftaux 1 + lift_from 1 n t ;; let subst arg = diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.mli b/helm/ocaml/cic_proof_checking/cicSubstitution.mli index 3aff92f96..9083212ae 100644 --- a/helm/ocaml/cic_proof_checking/cicSubstitution.mli +++ b/helm/ocaml/cic_proof_checking/cicSubstitution.mli @@ -33,6 +33,10 @@ exception ReferenceToInductiveDefinition;; (* lifts [t] of [n] *) val lift : int -> Cic.term -> Cic.term +(* lift from n t *) +(* as lift but lifts only indexes >= from *) +val lift_from: int -> int -> Cic.term -> Cic.term + (* subst t1 t2 *) (* substitutes [t1] for [Rel 1] in [t2] *) val subst : Cic.term -> Cic.term -> Cic.term -- 2.39.2