blob: 53adc2981c6b27ce7a270fb09eed8df56665d8cf (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
Fixpoint bug_1 (e1 : nat) {struct e1}
: nat
with bug_2 {H_imp : nat} (e2 : nat) {struct e2}
: nat.
Proof.
- exact e1.
- exact e2.
Admitted.
Fixpoint hbug_1 (a:bool) (e1 : nat) {struct e1}
: nat
with hbug_2 (a:nat) (e2 : nat) {struct e2}
: nat.
Proof.
- exact e1.
- exact e2.
Admitted.
Check (hbug_1 : bool -> nat -> nat).
Check (hbug_2 : nat -> nat -> nat).
|
