← Back to branch summary

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

« back to all changes in this revision

Viewing changes to test/succeed/Issue137.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/Issue137.agda
1
 
{-# OPTIONS --no-termination-check #-}
2
 
module Issue137 where
3
 
 
4
 
record Foo : Set1 where
5
 
  field
6
 
    foo : {x : Set} → Set
7
 
 
8
 
record Bar : Set1 where
9
 
  field
10
 
    bar : Foo
11
 
 
12
 
record Baz (P : Bar) : Set1 where
13
 
  field
14
 
    baz : Set
15
 
 
16
 
postulate
17
 
  P : Bar
18
 
  Q : Baz P
19
 
 
20
 
f : Baz.baz Q → Set
21
 
f r with f r
22
 
f r | A = A
23
 
 
24
 
 
25