diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /test-suite/success/indelim.v | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'test-suite/success/indelim.v')
-rw-r--r-- | test-suite/success/indelim.v | 61 |
1 files changed, 61 insertions, 0 deletions
diff --git a/test-suite/success/indelim.v b/test-suite/success/indelim.v new file mode 100644 index 00000000..91b6dee2 --- /dev/null +++ b/test-suite/success/indelim.v @@ -0,0 +1,61 @@ +Inductive boolP : Prop := +| trueP : boolP +| falseP : boolP. + +Fail Check boolP_rect. + + +Inductive True : Prop := I : True. + +Inductive False : Prop :=. + +Inductive Empty_set : Set :=. + +Fail Inductive Large_set : Set := + large_constr : forall A : Set, A -> Large_set. + +Inductive smallunitProp : Prop := +| onlyProps : True -> smallunitProp. + +Check smallunitProp_rect. + +Inductive nonsmallunitProp : Prop := +| notonlyProps : nat -> nonsmallunitProp. + +Fail Check nonsmallunitProp_rect. +Set Printing Universes. +Inductive inferProp := +| hasonlyProps : True -> nonsmallunitProp -> inferProp. + +Check (inferProp : Prop). + +Inductive inferSet := +| hasaset : nat -> True -> nonsmallunitProp -> inferSet. + +Fail Check (inferSet : Prop). + +Check (inferSet : Set). + +Inductive inferLargeSet := +| hasalargeset : Set -> True -> nonsmallunitProp -> inferLargeSet. + +Fail Check (inferLargeSet : Set). + +Inductive largeProp : Prop := somelargeprop : Set -> largeProp. + + +Inductive comparison : Set := + | Eq : comparison + | Lt : comparison + | Gt : comparison. + +Inductive CompareSpecT (Peq Plt Pgt : Prop) : comparison -> Type := + | CompEqT : Peq -> CompareSpecT Peq Plt Pgt Eq + | CompLtT : Plt -> CompareSpecT Peq Plt Pgt Lt + | CompGtT : Pgt -> CompareSpecT Peq Plt Pgt Gt. + +Inductive color := Red | Black. + +Inductive option (A : Type) : Type := +| None : option A +| Some : A -> option A.
\ No newline at end of file |