← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to benchmark/ac/Bool.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
benchmark/ac/Bool.agda
1
 
 
2
 
module Bool where
3
 
 
4
 
import Logic
5
 
open Logic
6
 
 
7
 
data Bool : Set where
8
 
  false : Bool
9
 
  true  : Bool
10
 
 
11
 
{-# BUILTIN BOOL Bool #-}
12
 
{-# BUILTIN FALSE false #-}
13
 
{-# BUILTIN TRUE true #-}
14
 
 
15
 
infixr 5 _&&_
16
 
 
17
 
_&&_ : Bool -> Bool -> Bool
18
 
true  && x = x
19
 
false && _ = false
20
 
 
21
 
not : Bool -> Bool
22
 
not true  = false
23
 
not false = true
24
 
 
25
 
IsTrue : Bool -> Set
26
 
IsTrue true  = True
27
 
IsTrue false = False
28
 
 
29
 
IsFalse : Bool -> Set
30
 
IsFalse x = IsTrue (not x)
31
 
 
32
 
module BoolEq where
33
 
 
34
 
  _==_ : Bool -> Bool -> Bool
35
 
  true  == x = x
36
 
  false == x = not x
37
 
 
38
 
  subst : {x y : Bool}(P : Bool -> Set) -> IsTrue (x == y) -> P x -> P y
39
 
  subst {true}{true}   _ _ px = px
40
 
  subst {false}{false} _ _ px = px
41
 
  subst {true}{false}  _ () _
42
 
  subst {false}{true}  _ () _
43
 
 
44
 
  isTrue== : {x : Bool} -> IsTrue x -> IsTrue (x == true)
45
 
  isTrue== {true} _ = tt
46
 
  isTrue== {false} ()
47
 
 
48
 
infix 1 if_then_else_
49
 
 
50
 
if_then_else_ : {A : Set} -> Bool -> A -> A -> A
51
 
if true  then x else y = x
52
 
if false then x else y = y
53
 
 
54
 
open BoolEq
55
 
 
56
 
if'_then_else_ : {A : Set} -> (x : Bool) -> (IsTrue x -> A) -> (IsFalse x -> A) -> A
57
 
if' true  then f else g = f tt
58
 
if' false then f else  g = g tt
59
 
 
60
 
isTrue&&₁ : {x y : Bool} -> IsTrue (x && y) -> IsTrue x
61
 
isTrue&&₁ {true} _ = tt
62
 
isTrue&&₁ {false} ()
63
 
 
64
 
isTrue&&₂ : {x y : Bool} -> IsTrue (x && y) -> IsTrue y
65
 
isTrue&&₂ {true} p = p
66
 
isTrue&&₂ {false} ()
67