blob: 3f1ab96fe184a77179ad5bf3af93b896e915ca6b (
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
|
Axiom checker_flags : Set.
Inductive Box (R : Type) : Type := box : Box R.
Inductive typing (H : checker_flags) : Type :=
| type_Rel : typing H -> typing H
| type_Case : let i := tt in Box (typing H) -> typing H.
Definition unbox (P : Type) (b : Box P) := match b with box _ => 0 end.
Definition size (H : checker_flags) (d : typing H) : nat.
Proof.
revert d.
fix size 1.
destruct 1.
- exact (size d).
- exact (unbox _ b).
Defined.
Definition foo (H : checker_flags) (a : typing H) :
size H (type_Rel H a) = size H a.
Proof.
simpl.
reflexivity.
Qed.
Definition bar (H : checker_flags) (a : typing H) :
size H (type_Rel H a) = size H a.
Proof.
vm_compute.
reflexivity.
Qed.
Definition qux (H : checker_flags) (a : typing H) :
size H (type_Rel H a) = size H a.
Proof.
native_compute.
reflexivity.
Qed.
|
