aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/HoTT_coq_077.v
blob: 017780c1f3567a12dc63890400018bb512c9fdb2 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
Set Implicit Arguments.

Require Import Logic.

Set Asymmetric Patterns.
Set Record Elimination Schemes.
Set Primitive Projections.

Record prod (A B : Type) : Type :=
  pair { fst : A; snd : B }.

Print prod_rect.
(** prod_rect =
fun (A B : Type) (P : prod A B -> Type)
  (f : forall (fst : A) (snd : B), P {| fst := fst; snd := snd |})
  (p : prod A B) =>
match p as p0 return (P p0) with
| {| fst := x; snd := x0 |} => f x x0
end
     : forall (A B : Type) (P : prod A B -> Type),
       (forall (fst : A) (snd : B), P {| fst := fst; snd := snd |}) ->
       forall p : prod A B, P p

Arguments A, B are implicit
Argument scopes are [type_scope type_scope _ _ _]
 *)

(* 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).

Notation typeof x := (ltac:(let T := type of x in exact T)) (only parsing).

(* Check for eta *)
Check eq_refl : typeof (@prod_rect) = typeof (@prod_rect').

(* Check for the recursion principle I want *)
Check eq_refl : @prod_rect = @prod_rect'.