blob: 15e43b7fb9347042e6a997f4e87afd204f55d5d9 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
- : constr =
constr:((fix add (n m : nat) {struct n} : nat :=
match n with
| 0 => m
| S p => S (add p m)
end) (1 + 2) 3)
- : constr = constr:(S (0 + 2 + 3))
- : constr = constr:(6)
- : constr = constr:(1 + 2 + 3)
- : constr = constr:(6)
- : constr = constr:(1 + 2 + 3)
- : constr = constr:(1 + 2 + 3)
- : constr = constr:(6)
- : constr = constr:(1 + 2 + 3)
- : constr = constr:(1 + 2 + 3)
- : constr = constr:(6)
- : constr = constr:(1 + 2 + 3)
- : constr = constr:(1 + 2 + 3)
- : constr list = [constr:(0 <> 0); constr:(0 = 0 -> False);
constr:((fun P : Prop => P -> False) (0 = 0)); constr:(
0 <> 0)]
|
