blob: 5f16d20cee34d43c64aa9372b818a6f141746c20 (
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
|
def id (A : type) (x : A) : A := x
def not (x : bool) : bool :=
bool-elim x at _ -> bool [
true => false,
false => true
]
def and (x : bool) (y : bool) : bool :=
bool-elim x at _ -> bool [
true => bool-elim y at _ -> bool [
true => true,
false => false
],
false => false
]
def or (x : bool) (y : bool) : bool :=
bool-elim x at _ -> bool [
true => true,
false => bool-elim y at _ -> bool [
true => true,
false => false
]
]
def xor (x : bool) (y : bool) : bool :=
or (and x (not y))
(and (not x) y)
|