From 82f61808091c59aa884eb232b96ee1c655dcb39a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 15 Dec 2008 13:12:28 +0000 Subject: [PATCH] aded some whd, you should be able to declare something like: inductive A : FOO := where FOO is defined as a sort (or unfolds to somthing ending with a sort) --- helm/software/components/library/cicElim.ml | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/helm/software/components/library/cicElim.ml b/helm/software/components/library/cicElim.ml index aacace7b5..282383d78 100644 --- a/helm/software/components/library/cicElim.ml +++ b/helm/software/components/library/cicElim.ml @@ -150,14 +150,20 @@ let rec mk_rels consno = function | 0 -> [] | n -> Cic.Rel (n+consno) :: mk_rels consno (n-1) -let rec strip_pi = function - | Cic.Prod (_, _, tgt) -> strip_pi tgt +let rec strip_pi ctx t = + match CicReduction.whd ~delta:true ctx t with + | Cic.Prod (n, s, tgt) -> strip_pi (Some (n,Cic.Decl s) :: ctx) tgt | t -> t -let rec count_pi = function - | Cic.Prod (_, _, tgt) -> count_pi tgt + 1 +let strip_pi t = strip_pi [] t + +let rec count_pi ctx t = + match CicReduction.whd ~delta:true ctx t with + | Cic.Prod (n, s, tgt) -> count_pi (Some (n,Cic.Decl s)::ctx) tgt + 1 | t -> 0 +let count_pi t = count_pi [] t + let rec type_of_p sort dependent leftno indty = function | Cic.Prod (n, src, tgt) when leftno = 0 -> let n = -- 2.39.2