bool.why 671 Bytes
Newer Older
1

2
theory Bool
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

  type bool = True | False

  logic andb(x:bool, y:bool) : bool = 
    match x, y with
    | True, True -> True
    | _   , _    -> False
    end

  logic orb(x:bool, y:bool) : bool = 
    match x, y with
    | False, False -> False
    | _    , _     -> True
    end

  logic xorb(x:bool, y:bool) : bool = 
    match x, y with
    | True,  False -> True
    | False, True  -> True
    | _    , _     -> False
    end

  logic notb(x:bool) : bool = 
    match x with
    | False -> True
    | True  -> False
    end

end

theory Ite

35
  use import Bool
36
37
38
39
40
41
42
43

  logic ite(b:bool, x:'a, y:'a) : 'a = 
    match b with
    | True  -> x
    | False -> y
    end

end