diff options
author | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-04 00:39:49 +0200 |
---|---|---|
committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-04 01:13:33 +0200 |
commit | cd10b70637dea3cbba5785d163bc567a32a031a8 (patch) | |
tree | 046d26c33c0b9a0a58bdf6d0d56c5e5dcaf919cd /test-suite/bugs/closed/3481.v | |
parent | 593dfd66a5016ba457b6dccf1179a0e1ec7bff84 (diff) |
Add test suite files for closed bugs.
Diffstat (limited to 'test-suite/bugs/closed/3481.v')
-rw-r--r-- | test-suite/bugs/closed/3481.v | 70 |
1 files changed, 70 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3481.v b/test-suite/bugs/closed/3481.v new file mode 100644 index 000000000..1f180cd94 --- /dev/null +++ b/test-suite/bugs/closed/3481.v @@ -0,0 +1,70 @@ + +Set Implicit Arguments. + +Require Import Logic. +Module NonPrim. +Local Set Record Elimination Schemes. +Record prodwithlet (A B : Type) : Type := + pair' { fst : A; fst' := fst; snd : B }. + +Definition letreclet (p : prodwithlet nat nat) := + let (x, x', y) := p in x + y. + +Definition pletreclet (p : prodwithlet nat nat) := + let 'pair' x x' y := p in x + y + x'. + +Definition pletreclet2 (p : prodwithlet nat nat) := + let 'pair' x y := p in x + y. + +Check (pair 0 0). +End NonPrim. + +Global Set Universe Polymorphism. +Global Set Asymmetric Patterns. +Local Set Record Elimination Schemes. +Local Set Primitive Projections. + +Record prod (A B : Type) : Type := + pair { fst : A; snd : B }. + +Print prod_rect. + +(* What I really want: *) +Definition prod_rect' A B (P : prod A B -> Type) (u : forall (fst : A) (snd : B), P (pair fst snd)) + (p : prod A B) : P p + := u (fst p) (snd p). + +Definition conv : @prod_rect = @prod_rect'. +Proof. reflexivity. Defined. + +Fail Definition imposs := + (fun A B P f (p : prod A B) => match p as p0 return P p0 with + | {| fst := x ; snd := x0 |} => f x x0 + end). + +Definition letrec (p : prod nat nat) := + let (x, y) := p in x + y. +Eval compute in letrec (pair 1 5). + +Goal forall p : prod nat nat, letrec p = fst p + snd p. +Proof. + reflexivity. + Undo. + intros p. + case p. simpl. unfold letrec. simpl. reflexivity. +Defined. + +Eval compute in conv. (* = eq_refl + : prod_rect = prod_rect' *) + +Check eq_refl : @prod_rect = @prod_rect'. (* Toplevel input, characters 6-13: +Error: +The term "eq_refl" has type "prod_rect = prod_rect" +while it is expected to have type "prod_rect = prod_rect'" +(cannot unify "prod_rect" and "prod_rect'"). *) + +Record sigma (A : Type) (B : A -> Type) : Type := + dpair { pi1 : A ; pi2 : B pi1 }. + + + |