diff options
author | Matthieu Sozeau <mattam@mattam.org> | 2014-06-04 17:18:58 +0200 |
---|---|---|
committer | Matthieu Sozeau <mattam@mattam.org> | 2014-06-04 17:18:58 +0200 |
commit | dbada2989e334756971c7bf69578c93b2e45643e (patch) | |
tree | 9ee0e5de226b95f7ac0795ee1018e666a27fc897 /test-suite/success/namedunivs.v | |
parent | 332f092e3a30f8428b28f12c85c0a90e3f6d7171 (diff) |
- Better parsing and printing of named universes: Type{ident} and foo@{(ident|Prop|Set|Type|' ')*}
(user given names are still write only).
- Add test-suite file for named universes.
Diffstat (limited to 'test-suite/success/namedunivs.v')
-rw-r--r-- | test-suite/success/namedunivs.v | 100 |
1 files changed, 100 insertions, 0 deletions
diff --git a/test-suite/success/namedunivs.v b/test-suite/success/namedunivs.v new file mode 100644 index 000000000..62ee5519d --- /dev/null +++ b/test-suite/success/namedunivs.v @@ -0,0 +1,100 @@ +(* Inductive paths {A} (x : A) : A -> Type := idpath : paths x x where "x = y" := (@paths _ x y) : type_scope. *) +(* Goal forall A B : Set, @paths Type A B -> @paths Set A B. *) +(* intros A B H. *) +(* Fail exact H. *) +(* Abort . *) + +Section lift_strict. +Polymorphic Definition liftlt := + let t := Type{i} : Type{k} in + fun A : Type{i} => A : Type{k}. + +Polymorphic Definition liftle := + fun A : Type{i} => A : Type{k}. +End lift_strict. + + +Set Universe Polymorphism. + +(* Inductive option (A : Type) : Type := *) +(* | None : option A *) +(* | Some : A -> option A. *) + +Inductive option (A : Type{i}) : Type{i} := + | None : option A + | Some : A -> option A. + +Definition foo' {A : Type{i}} (o : option@{i} A) : option@{i} A := + o. + +Definition foo'' {A : Type{i}} (o : option@{j} A) : option@{k} A := + o. + +(* Inductive prod (A : Type{i}) (B : Type{j}) := *) +(* | pair : A -> B -> prod A B. *) + +(* Definition snd {A : Type{i}} (B : Type{j}) (p : prod A B) : B := *) +(* match p with *) +(* | pair _ _ a b => b *) +(* end. *) + +(* Definition snd' {A : Type{i}} (B : Type{i}) (p : prod A B) : B := *) +(* match p with *) +(* | pair _ _ a b => b *) +(* end. *) + + +(* Inductive paths {A : Type} : A -> A -> Type := *) +(* | idpath (a : A) : paths a a. *) + +Inductive paths {A : Type{i}} : A -> A -> Type{i} := +| idpath (a : A) : paths a a. + +Definition Funext := + forall (A : Type) (B : A -> Type), + forall f g : (forall a, B a), (forall x : A, paths (f x) (g x)) -> paths f g. + +Definition paths_lift_closed (A : Type{i}) (x y : A) : + paths x y -> @paths (liftle@{j Type} A) x y. +Proof. + intros. destruct X. exact (idpath _). +Defined. + +Definition paths_lift (A : Type{i}) (x y : A) : + paths x y -> paths@{j} x y. +Proof. + intros. destruct X. exact (idpath _). +Defined. + +Definition paths_lift_closed_strict (A : Type{i}) (x y : A) : + paths x y -> @paths (liftlt@{j Type} A) x y. +Proof. + intros. destruct X. exact (idpath _). +Defined. + +Definition paths_downward_closed_le (A : Type{i}) (x y : A) : + paths@{j} (A:=liftle@{i j} A) x y -> paths@{i} x y. +Proof. + intros. destruct X. exact (idpath _). +Defined. + +Definition paths_downward_closed_lt (A : Type{i}) (x y : A) : + @paths (liftlt@{j i} A) x y -> paths x y. +Proof. + intros. destruct X. exact (idpath _). +Defined. + +Definition paths_downward_closed_lt_nolift (A : Type{i}) (x y : A) : + paths@{j} x y -> paths x y. +Proof. + intros. destruct X. exact (idpath _). +Defined. + +Definition funext_downward_closed (F : Funext@{i' j' k'}) : + Funext@{i j k}. +Proof. + intros A B f g H. red in F. + pose (F A B f g (fun x => paths_lift _ _ _ (H x))). + apply paths_downward_closed_lt_nolift. apply p. +Defined. + |