← Back to branch summary

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

« back to all changes in this revision

Viewing changes to examples/outdated-and-incorrect/cbs/Basics.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:
examples/outdated-and-incorrect/cbs/Basics.agda
1
 
 
2
 
module Basics where
3
 
 
4
 
_%_ : {A B : Set}{C : B -> Set}
5
 
      (f : (x : B) -> C x)(g : A -> B)(x : A) -> C (g x)
6
 
f % g = \x -> f (g x)
7
 
 
8
 
 
9
 
data   False : Set where
10
 
record True  : Set where
11
 
 
12
 
tt : True
13
 
tt = _
14
 
 
15
 
¬_ : Set -> Set
16
 
¬ A = A -> False
17
 
 
18
 
record ∃ {A : Set}(P : A -> Set) : Set where
19
 
  field
20
 
    witness : A
21
 
    proof   : P witness
22
 
 
23
 
∃-intro : {A : Set}{P : A -> Set}(x : A) -> P x -> ∃ P
24
 
∃-intro x p = record { witness = x; proof = p }
25
 
 
26
 
infixr 15 _/\_ _×_
27
 
 
28
 
data _×_ (A B : Set) : Set where
29
 
  _,_ : A -> B -> A × B
30
 
 
31
 
_/\_ = _×_
32
 
 
33
 
 
34
 
data Lift (A : Set) : Set where
35
 
  bot  : Lift A
36
 
  lift : A -> Lift A
37
 
 
38
 
_=<<_ : {A B : Set} -> (A -> Lift B) -> Lift A -> Lift B
39
 
f =<< bot    = bot
40
 
f =<< lift v = f v
41
 
 
42
 
 
43
 
data Nat : Set where
44
 
  zero : Nat
45
 
  suc  : Nat -> Nat
46
 
 
47
 
 
48
 
infix 10 _==_
49
 
 
50
 
data _==_ {A : Set}(x : A) : A -> Set where
51
 
  refl : x == x
52
 
 
53
 
data Id {A : Set}(x : A) : Set where
54
 
  it : (y : A) -> x == y -> Id x
55
 
 
56
 
 
57
 
data Bool : Set where
58
 
  true  : Bool
59
 
  false : Bool
60
 
 
61
 
data LR : Set where
62
 
  left  : LR
63
 
  right : LR
64
 
 
65
 
if_then_else_ : {A : Set} -> Bool -> A -> A -> A
66
 
if true  then x else y = x
67
 
if false then x else y = y
68
 
 
69
 
 
70
 
infixr 50 _::_
71
 
 
72
 
data List (A : Set) : Set where
73
 
  []   : List A
74
 
  _::_ : A -> List A -> List A
75
 
 
76
 
data Elem {A : Set}(x : A) : List A -> Set where
77
 
  hd : forall {xs} -> Elem x (x :: xs)
78
 
  tl : forall {y xs} -> Elem x xs -> Elem x (y :: xs)