← Back to branch summary

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

« back to all changes in this revision

Viewing changes to test/succeed/Issue462.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/Issue462.agda
1
 
module Issue462 where
2
 
 
3
 
data _≡_ {A : Set} : A → A → Set where
4
 
  ≡-refl : (x : A) → x ≡ x
5
 
 
6
 
postulate A : Set
7
 
 
8
 
record R (_≈_ _∼_ : A → A → Set) : Set where
9
 
  field
10
 
    ≈-refl      : (x : A) → x ≈ x
11
 
    ∼-reflexive : (x y : A) → x ≈ y → x ∼ y
12
 
 
13
 
  ∼-refl : (x : A) → x ∼ x
14
 
  ∼-refl x = ∼-reflexive x x (≈-refl x)
15
 
 
16
 
postulate
17
 
  _≈_    : A → A → Set
18
 
  ≈-refl : ((x : A) → x ≡ x) → (x : A) → x ≈ x
19
 
  ≈-irr  : (x : A) (p : x ≈ x) → p ≡ p
20
 
 
21
 
≡-r : R _≡_ _≡_
22
 
≡-r = record
23
 
  { ≈-refl      = ≡-refl
24
 
  ; ∼-reflexive = λ _ _ p → p
25
 
  }
26
 
 
27
 
≈-reflexive : (x y : A) → x ≡ y → x ≈ y
28
 
≈-reflexive .x .x (≡-refl x) = ≈-refl (R.∼-refl ≡-r) x
29
 
 
30
 
≈-r : R _≡_ _≈_
31
 
≈-r = record
32
 
  { ≈-refl      = ≡-refl
33
 
  ; ∼-reflexive = ≈-reflexive
34
 
  }
35
 
 
36
 
foo : A → Set₁
37
 
foo x with ≈-irr x (R.∼-refl ≈-r x)
38
 
foo x | _ = Set
39