diff options
author | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-04 21:52:08 +0200 |
---|---|---|
committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-05 10:01:07 +0200 |
commit | 8c54bdeec740fb9edd80e28ce743418bf1276b90 (patch) | |
tree | 744cea8877f75bb440a61d815af6c59821f9cc65 /test-suite/success/primitiveproj.v | |
parent | 080167469f6435696d785caa1fca9fd258148157 (diff) |
Fix primitive projections declarations for inductive records.
Diffstat (limited to 'test-suite/success/primitiveproj.v')
-rw-r--r-- | test-suite/success/primitiveproj.v | 33 |
1 files changed, 33 insertions, 0 deletions
diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v index 2682df3b7..4a9c81eb3 100644 --- a/test-suite/success/primitiveproj.v +++ b/test-suite/success/primitiveproj.v @@ -28,3 +28,36 @@ Section bla. End bla. End Univ. + +Set Primitive Projections. +Unset Elimination Schemes. +Set Implicit Arguments. + +Check nat. + +(* Inductive X (U:Type) := Foo (k : nat) (x : X U). *) +(* Parameter x : X nat. *) +(* Check x.(k). *) + +Inductive X (U:Type) := { k : nat; a: k = k -> X U; b : let x := a eq_refl in X U }. + +Parameter x:X nat. +Check (a x : forall _ : @eq nat (k x) (k x), X nat). +Check (b x : X nat). + +Inductive Y := { next : option Y }. + +Check _.(next) : option Y. +Lemma eta_ind (y : Y) : y = Build_Y y.(next). +Proof. reflexivity. Defined. + +Variable t : Y. + +Fixpoint yn (n : nat) (y : Y) : Y := + match n with + | 0 => t + | S n => {| next := Some (yn n y) |} + end. + +Lemma eta_ind' (y: Y) : Some (yn 100 y) = Some {| next := (yn 100 y).(next) |}. +Proof. reflexivity. Defined. |