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
|
Module Single.
Inductive bexp : Set :=
| b_true : bexp
| b_false : bexp
| b_eq : bexp -> bexp -> bexp.
Class ContainsFalse (A : Set) :=
contains_false : A -> bool.
Fixpoint bexp_CF : ContainsFalse bexp := fun b =>
match b with
| b_true => false
| b_false => true
| b_eq a1 a2 => orb (contains_false a1) (contains_false a2)
end.
Existing Instance bexp_CF.
End Single.
Module Mutual.
Inductive bexp : Set :=
| b_true : bexp
| b_false : bexp
| b_eq : aexp -> aexp -> bexp
with aexp : Set :=
| a_of_bool : bexp -> aexp.
Class ContainsFalse (A : Set) :=
contains_false : A -> bool.
Fixpoint bexp_ContainsFalse : ContainsFalse bexp := fun b =>
match b with
| b_true => false
| b_false => true
| b_eq a1 a2 => orb (contains_false a1) (contains_false a2)
end with
aexp_ContainsFalse : ContainsFalse aexp := fun a =>
match a with
| a_of_bool b => contains_false b
end.
Existing Instance bexp_ContainsFalse.
Existing Instance aexp_ContainsFalse.
End Mutual.
|
