blob: 120e62b14537f9a7a1f92f03de46628cffb8f7dc (
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
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
|
Require Import Program.
Axiom bogus : Type.
Section A.
Variable x : bogus.
#[using="All"]
Definition c1 : bool := true.
#[using="All"]
Fixpoint c2 n : bool :=
match n with
| O => true
| S p => c3 p
end
with c3 n : bool :=
match n with
| O => true
| S p => c2 p
end.
#[using="All"]
Definition c4 : bool. Proof. exact true. Qed.
#[using="All"]
Fixpoint c5 (n : nat) {struct n} : bool. Proof. destruct n as [|p]. exact true. exact (c5 p). Qed.
#[using="All", program]
Definition c6 : bool. Proof. exact true. Qed.
#[using="All", program]
Fixpoint c7 (n : nat) {struct n} : bool :=
match n with
| O => true
| S p => c7 p
end.
End A.
Check c1 : bogus -> bool.
Check c2 : bogus -> nat -> bool.
Check c3 : bogus -> nat -> bool.
Check c4 : bogus -> bool.
Check c5 : bogus -> nat -> bool.
Check c6 : bogus -> bool.
Check c7 : bogus -> nat -> bool.
Section B.
Variable a : bogus.
Variable h : c1 a = true.
#[using="a*"]
Definition c8 : bogus := a.
Collection ccc := a h.
#[using="ccc"]
Definition c9 : bogus := a.
#[using="ccc - h"]
Definition c10 : bogus := a.
End B.
Check c8 : forall a, c1 a = true -> bogus.
Check c9 : forall a, c1 a = true -> bogus.
Check c10: bogus -> bogus.
|
