← Back to branch summary

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

« back to all changes in this revision

Viewing changes to test/epic/tests/Forcing2.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:
test/epic/tests/Forcing2.agda
1
 
module tests.Forcing2 where
2
 
 
3
 
open import Prelude.Nat
4
 
open import Prelude.IO
5
 
open import Prelude.Unit
6
 
 
7
 
data _**_ (A B : Set) : Set where
8
 
  _,_ : A -> B -> A ** B
9
 
 
10
 
data P {A B : Set} : A ** B -> Set where
11
 
  _,_ : (x : A)(y : B) -> P (x , y)
12
 
 
13
 
data Q {A : Set} : A ** A -> Set where
14
 
  [_] : (x : A) -> Q (x , x)
15
 
 
16
 
test1 : (p : Nat ** Nat) -> P p -> Nat
17
 
test1 .(x , y) (x , y) = x + y
18
 
 
19
 
test2 : (q : Nat ** Nat) -> Q q -> Nat
20
 
test2 .(x , x) [ x ]  = ((S (S Z)) * x) + 1
21
 
 
22
 
 
23
 
test3 : (q : (Nat ** Nat) ** (Nat ** Nat)) -> Q q -> Nat
24
 
test3 .((Z , Z)   , (Z , Z))   [ Z   , Z ]  = Z
25
 
test3 .((S n , m) , (S n , m)) [ S n , m ]  = S n + m
26
 
test3 .((Z , m)   , (Z , m))   [ Z   , m ]  = m
27
 
main : IO Unit 
28
 
main = 
29
 
    printNat (test1 (5  , 8) (5  , 8)) ,,
30
 
    printNat (test2 (1 , 1) [ 1 ])     ,,
31
 
    printNat (test3 ( (3 , 4) , (3 , 4) ) [ 3 , 4 ]) ,,
32
 
    return unit