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
|
(* additional test cases for manual testing *)
Goal 1 + 1 = 3 -> False -> True.
intro. clear H; intro.
Abort.
Goal nat -> bool -> nat -> True.
intros i b j.
revert b.
cbn.
Abort.
Require Import Coq.Init.Number.
Goal int -> uint -> nat -> nat -> nat -> nat ->True.
intros a b c.
clear a b c; intros b a c.
Abort.
Goal int -> nat -> uint -> nat -> nat -> nat -> True.
intros a b c.
clear a b c; intros c a b.
Abort.
Goal uint -> int -> nat -> nat -> nat -> nat -> True.
intros a b c. clear a b c; intros b a c.
Abort.
Goal nat -> int -> int -> nat -> nat -> int -> True.
intros a c d. clear a c d; intros a b d.
Abort.
Goal 1 = 0 -> True -> False -> True.
intros X H. clear H; intro.
Abort.
Goal True -> True -> False -> False -> True.
intros H H0. clear H H0; intros H H0.
Abort.
Goal True -> True -> False -> False -> False
-> True.
intros H H0. clear H H0; intros H H0 H1.
Abort.
|
