← Back to branch summary

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

« back to all changes in this revision

Viewing changes to test/succeed/IrrelevantRecordFields.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/IrrelevantRecordFields.agda
1
 
 
2
 
{-# OPTIONS --no-irrelevant-projections #-}
3
 
 
4
 
module IrrelevantRecordFields where
5
 
 
6
 
  
7
 
infix 4 _≡_ 
8
 
 
9
 
data _≡_ {A : Set}(a : A) : A -> Set where
10
 
  refl : a ≡ a
11
 
 
12
 
sym : {A : Set}{a b : A} → a ≡ b → b ≡ a
13
 
sym refl = refl
14
 
 
15
 
record SemiG : Set1 where
16
 
 constructor _,_,_,_,_,_
17
 
 field
18
 
   M    : Set
19
 
   unit : M
20
 
   _+_  : M -> M -> M
21
 
   .assoc     : ∀ {x y z} ->  x + (y + z) ≡ (x + y) + z
22
 
   .leftUnit  : ∀ {x} -> unit + x ≡ x
23
 
   .rightUnit : ∀ {x} -> x + unit ≡ x
24
 
 
25
 
dual : SemiG -> SemiG
26
 
dual (M , e , _+_ , assoc , leftUnit , rightUnit) = 
27
 
  M , e , (λ x y -> y + x) , sym assoc , rightUnit , leftUnit
28
 
 
29
 
data _≡₁_ {A : Set1}(a : A) : A -> Set where
30
 
  refl : a ≡₁ a
31
 
 
32
 
open SemiG
33
 
 
34
 
 
35
 
dual∘dual≡id : ∀ M -> dual (dual M) ≡₁ M
36
 
dual∘dual≡id M = refl {a = M}
37
 
 
38
 
 
39