← Back to branch summary

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

« back to all changes in this revision

Viewing changes to examples/SummerSchool07/Lecture/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/SummerSchool07/Lecture/Basics.agda
1
 
{-
2
 
 
3
 
          Types Summer School 2007
4
 
 
5
 
                 Bertinoro
6
 
             Aug 19 - 31, 2007
7
 
 
8
 
 
9
 
                   Agda
10
 
 
11
 
                Ulf Norell
12
 
 
13
 
-}
14
 
 
15
 
{-
16
 
 
17
 
  Learn more about Agda on the Agda wiki:
18
 
 
19
 
    http://www.cs.chalmers.se/~ulfn/Agda
20
 
 
21
 
  This is where you find the exercises for the afternoon.
22
 
 
23
 
-}
24
 
 
25
 
 
26
 
module Basics where
27
 
 
28
 
{-
29
 
 
30
 
  Expressions (types and terms)
31
 
 
32
 
-}
33
 
 
34
 
 
35
 
id₁ : (A : Set) -> A -> A
36
 
id₁ = \ A x -> x
37
 
 
38
 
id₂ : (A : Set) -> A -> A
39
 
id₂ = \ A x -> id₁ A (id₁ A x)
40
 
 
41
 
 
42
 
 
43
 
compose : (A B C : Set) -> (B -> C) -> (A -> B) -> A -> C
44
 
compose = \(A B C : Set) f g x -> f (g x)
45
 
 
46
 
compose' : (A B : Set)(C : B -> Set)
47
 
           (f : (x : B) -> C x)(g : A -> B) ->
48
 
           (x : A) -> C (g x)
49
 
compose' = \A B C f g x -> f (g x)
50
 
 
51
 
{-
52
 
 
53
 
  Implicit arguments
54
 
 
55
 
-}
56
 
 
57
 
 
58
 
id₃ : {A : Set} -> A -> A
59
 
id₃ = \ x -> x
60
 
 
61
 
id₄ : {A : Set} -> A -> A
62
 
id₄ = \ x -> (id₃ (id₃ x))
63
 
 
64
 
id₆ : {A : Set} -> A -> A
65
 
id₆ x = id₁ _ x
66
 
 
67