However, it is not Type0, but a moving Type as usual, for example
inductive and (A,B:CProp) : CProp := ...
inductive exists (A:Type) (P:A->CProp) : CProp :=
| ext : \forall x:A. \forall p : P x. exists A P.
does not pass since the sort of x is Type not included in CProp. Putting
exists in Type does not work either, if you want to make a conjuction
involving an existential.
solution, to be implemented:
CProp of CicUniv.universe
where CProp n is meant to be Type (n + 0.5).
let t1' = CicReduction.whd ~subst context t1 in
let t2' = CicReduction.whd ~subst ((Some (name,C.Decl s))::context) t2 in
match (t1', t2') with
let t1' = CicReduction.whd ~subst context t1 in
let t2' = CicReduction.whd ~subst ((Some (name,C.Decl s))::context) t2 in
match (t1', t2') with
- (C.Sort s1, C.Sort s2)
- when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
+ | (C.Sort s1, C.Sort (C.Prop | C.Set)) ->
(* different from Coq manual!!! *)
(* different from Coq manual!!! *)
+ t2',ugraph
+ | (C.Sort (C.Prop | C.Set | C.CProp), C.Sort C.CProp ) -> t2', ugraph
| (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
(* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
let t' = CicUniv.fresh() in
| (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
(* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
let t' = CicUniv.fresh() in
C.Sort (C.Type t'),ugraph2
with
CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg))
C.Sort (C.Type t'),ugraph2
with
CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg))
- | (C.Sort _,C.Sort (C.Type t1)) ->
+ | (C.Sort _,C.Sort (C.Type t1))
+ | (C.Sort (C.Type t1), C.Sort C.CProp) ->
(* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
C.Sort (C.Type t1),ugraph (* c'e' bisogno di un fresh? *)
| (C.Meta _, C.Sort _) -> t2',ugraph
(* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
C.Sort (C.Type t1),ugraph (* c'e' bisogno di un fresh? *)
| (C.Meta _, C.Sort _) -> t2',ugraph