diff options
Diffstat (limited to 'test-suite/success/primitiveproj.v')
| -rw-r--r-- | test-suite/success/primitiveproj.v | 18 |
1 files changed, 3 insertions, 15 deletions
diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v index 281d707c..2fa77049 100644 --- a/test-suite/success/primitiveproj.v +++ b/test-suite/success/primitiveproj.v @@ -35,10 +35,6 @@ 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. @@ -49,19 +45,11 @@ 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. +Proof. Fail reflexivity. Abort. -Lemma eta_ind' (y: Y) : Some (yn 100 y) = Some {| next := (yn 100 y).(next) |}. -Proof. reflexivity. Defined. +Inductive Fdef := { Fa : nat ; Fb := Fa; Fc : Fdef }. +Fail Scheme Fdef_rec := Induction for Fdef Sort Prop. (* Rules for parsing and printing of primitive projections and their eta expansions. |