← Back to branch summary

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

« back to all changes in this revision

Viewing changes to test/succeed/Issue354.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/Issue354.agda
1
 
 
2
 
{-# OPTIONS --universe-polymorphism #-}
3
 
 
4
 
module Issue354 where
5
 
 
6
 
------------------------------------------------------------------------
7
 
 
8
 
postulate
9
 
  Level : Set
10
 
  zero : Level
11
 
  suc  : (i : Level) → Level
12
 
  _⊔_ : Level → Level → Level
13
 
 
14
 
{-# BUILTIN LEVEL     Level #-}
15
 
{-# BUILTIN LEVELZERO zero  #-}
16
 
{-# BUILTIN LEVELSUC  suc   #-}
17
 
{-# BUILTIN LEVELMAX  _⊔_   #-}
18
 
 
19
 
data _≡_ {a} {A : Set a} (x : A) : A → Set a where
20
 
  refl : x ≡ x
21
 
 
22
 
_≗_ : ∀ {a b} {A : Set a} {B : Set b} (f g : A → B) → Set (a ⊔ b)
23
 
f ≗ g = ∀ x → f x ≡ g x
24
 
 
25
 
------------------------------------------------------------------------
26
 
 
27
 
postulate
28
 
  a     : Level
29
 
  A     : Set a
30
 
  P     : A → Set
31
 
  x     : A
32
 
  f     : ∀ {a} {A : Set a} → A → A
33
 
  g     : A → A
34
 
  lemma : f ≗ g
35
 
 
36
 
p : f x ≡ g x
37
 
p with f x | lemma x
38
 
... | .(g x) | refl = refl
39
 
 
40
 
 
41
 
--
42
 
--