← Back to branch summary

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

« back to all changes in this revision

Viewing changes to test/succeed/Issue558b.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/succeed/Issue558b.agda
1
 
module Issue558b where
2
 
 
3
 
data Nat : Set where
4
 
  Z : Nat
5
 
  S : Nat → Nat
6
 
 
7
 
data _≡_ {A : Set} (a : A) : A → Set where
8
 
  Refl : a ≡ a
9
 
 
10
 
plus : Nat → Nat → Nat
11
 
plus Z n = n
12
 
plus (S n) m = S (plus n m)
13
 
 
14
 
data Addable (τ : Set) : Set where
15
 
  addable : (τ → τ → τ) → Addable τ
16
 
 
17
 
plus' : {τ : Set} → Addable τ → τ → τ → τ
18
 
plus' (addable p) = p
19
 
 
20
 
record ⊤ : Set where
21
 
 
22
 
module AddableM {τ : Set} {a : ⊤} (a : Addable τ) where
23
 
  _+_ : τ → τ → τ
24
 
  _+_ = plus' a
25
 
 
26
 
 
27
 
open module AddableIFS {t : Set} {a : ⊤} {{r : Addable t}} = AddableM {t} r
28
 
 
29
 
data CommAddable (τ : Set) {a : ⊤} : Set where
30
 
 commAddable : (addable : Addable τ) → ((a b : τ) → (a + b) ≡ (b + a)) → CommAddable τ
31
 
 
32
 
private
33
 
  addableCA' : {τ : Set} (ca : CommAddable τ) → Addable τ
34
 
  addableCA' (commAddable a _) = a
35
 
 
36
 
  comm' : {τ : Set} (ca : CommAddable τ) →
37
 
          let a = addableCA' ca in (a b : τ) → (a + b) ≡ (b + a)
38
 
  comm' (commAddable _ c) = c
39
 
 
40
 
module CommAddableM {τ : Set} {a : ⊤} (ca : CommAddable τ) where
41
 
  addableCA : Addable τ
42
 
  addableCA = addableCA' ca
43
 
 
44
 
  comm : (a b : τ) → (a + b) ≡ (b + a)
45
 
  comm = comm' ca
46
 
 
47
 
natAdd : Addable Nat
48
 
natAdd = addable plus
49
 
 
50
 
postulate commPlus : (a b : Nat) → plus a b ≡ plus b a
51
 
 
52
 
commNatAdd : CommAddable Nat
53
 
commNatAdd = commAddable natAdd commPlus
54
 
 
55
 
open CommAddableM {{...}}
56
 
 
57
 
test : (Z + Z) ≡ Z
58
 
test = comm Z Z
59
 
 
60
 
a : {x y : Nat} → (S (S Z) + (x + y)) ≡ ((x + y) + S (S Z))
61
 
a {x}{y} = comm (S (S Z)) (x + y)