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
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
|
t_rect =
fun (P : t -> Type) (f : let x := t in forall x0 : x, P x0 -> P (k x0)) =>
fix F (t : t) : P t :=
match t as t0 return (P t0) with
| k _ x0 => f x0 (F x0)
end
: forall P : t -> Type,
(let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t
Argument scopes are [function_scope function_scope _]
= fun d : TT => match d with
| {| f3 := b |} => b
end
: TT -> 0 = 0
= fun d : TT => match d with
| {| f3 := b |} => b
end
: TT -> 0 = 0
proj =
fun (x y : nat) (P : nat -> Type) (def : P x) (prf : P y) =>
match Nat.eq_dec x y with
| left eqprf => match eqprf in (_ = z) return (P z) with
| eq_refl => def
end
| right _ => prf
end
: forall (x y : nat) (P : nat -> Type), P x -> P y -> P y
Argument scopes are [nat_scope nat_scope function_scope _ _]
foo =
fix foo (A : Type) (l : list A) {struct l} : option A :=
match l with
| nil => None
| x0 :: nil => Some x0
| x0 :: (_ :: _) as l0 => foo A l0
end
: forall A : Type, list A -> option A
Argument scopes are [type_scope list_scope]
uncast =
fun (A : Type) (x : I A) => match x with
| x0 <: _ => x0
end
: forall A : Type, I A -> A
Argument scopes are [type_scope _]
foo' = if A 0 then true else false
: bool
f =
fun H : B =>
match H with
| AC x =>
let b0 := b in
(if b0 as b return (P b -> True)
then fun _ : P true => Logic.I
else fun _ : P false => Logic.I) x
end
: B -> True
The command has indeed failed with message:
Non exhaustive pattern-matching: no clause found for pattern
gadtTy _ _
The command has indeed failed with message:
In environment
texpDenote : forall t : type, texp t -> typeDenote t
t : type
e : texp t
t1 : type
t2 : type
t0 : type
b : tbinop t1 t2 t0
e1 : texp t1
e2 : texp t2
The term "0" has type "nat" while it is expected to have type
"typeDenote t0".
fun '{{n, m, _}} => n + m
: J -> nat
fun '{{n, m, p}} => n + m + p
: J -> nat
fun '(D n m p q) => n + m + p + q
: J -> nat
The command has indeed failed with message:
The constructor D (in type J) expects 3 arguments.
lem1 =
fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl
: forall k : nat * nat, k = k
lem2 =
fun dd : bool => if dd as aa return (aa = aa) then eq_refl else eq_refl
: forall k : bool, k = k
Argument scope is [bool_scope]
lem3 =
fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl
: forall k : nat * nat, k = k
1 subgoal
x : nat
n, n0 := match x + 0 with
| 0 => 0
| S _ => 0
end : nat
e,
e0 := match x + 0 as y return (y = y) with
| 0 => eq_refl
| S n => eq_refl
end : x + 0 = x + 0
n1, n2 := match x with
| 0 => 0
| S _ => 0
end : nat
e1, e2 := match x return (x = x) with
| 0 => eq_refl
| S n => eq_refl
end : x = x
============================
x + 0 = 0
1 subgoal
p : nat
a,
a0 := match eq_refl as y in (_ = e) return (y = y /\ e = e) with
| eq_refl => conj eq_refl eq_refl
end : eq_refl = eq_refl /\ p = p
a1,
a2 := match eq_refl in (_ = e) return (p = p /\ e = e) with
| eq_refl => conj eq_refl eq_refl
end : p = p /\ p = p
============================
eq_refl = eq_refl
|
