← Back to branch summary

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

« back to all changes in this revision

Viewing changes to test/interaction/NiceGoals.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/interaction/NiceGoals.agda
1
 
 
2
 
{-# OPTIONS --universe-polymorphism #-}
3
 
 
4
 
module NiceGoals 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
 
------------------------------------------------------------------------
20
 
 
21
 
record RawMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
22
 
  infixl 7 _∙_
23
 
  infix  4 _≈_
24
 
  field
25
 
    Carrier : Set c
26
 
    _≈_     : Carrier → Carrier → Set ℓ
27
 
    _∙_     : Carrier → Carrier → Carrier
28
 
    ε       : Carrier
29
 
 
30
 
module M (rm : RawMonoid zero zero) where
31
 
 
32
 
  open RawMonoid rm
33
 
 
34
 
  thm : ∀ x → x ∙ ε ≈ x
35
 
  thm = {!!}
36
 
 
37
 
  -- agda2-goal-and-context:
38
 
 
39
 
  -- rm : RawMonoid zero zero
40
 
  -- ------------------------
41
 
  -- Goal: (x : RawMonoid.Carrier rm) →
42
 
  --       RawMonoid._≈_ rm (RawMonoid._∙_ rm x (RawMonoid.ε rm)) x
43
 
 
44
 
------------------------------------------------------------------------
45
 
 
46
 
record RawMonoid′ : Set₁ where
47
 
  infixl 7 _∙_
48
 
  infix  4 _≈_
49
 
  field
50
 
    Carrier : Set
51
 
    _≈_     : Carrier → Carrier → Set
52
 
    _∙_     : Carrier → Carrier → Carrier
53
 
    ε       : Carrier
54
 
 
55
 
 
56
 
module M′ (rm : RawMonoid′) where
57
 
 
58
 
  open RawMonoid′ rm
59
 
 
60
 
  thm′ : ∀ x → x ∙ ε ≈ x
61
 
  thm′ = {!!}
62
 
 
63
 
  -- agda2-goal-and-context:
64
 
 
65
 
  -- rm : RawMonoid′
66
 
  -- ---------------
67
 
  -- Goal: (x : Carrier) → x ∙ ε ≈ x
68
 
 
69
 
 
70
 
------------------------------------------------------------------------
71
 
 
72
 
 
73
 
record RawMonoid″ (Carrier : Set) : Set₁ where
74
 
  infixl 7 _∙_
75
 
  infix  4 _≈_
76
 
  field
77
 
    _≈_     : Carrier → Carrier → Set
78
 
    _∙_     : Carrier → Carrier → Carrier
79
 
    ε       : Carrier
80
 
 
81
 
data Bool : Set where
82
 
  true false : Bool
83
 
 
84
 
data List (A : Set) : Set where
85
 
  []  :                        List A
86
 
  _∷_ : (x : A)(xs : List A) → List A
87
 
 
88
 
module M″ (rm : RawMonoid″ (List Bool)) where
89
 
 
90
 
  open RawMonoid″ rm
91
 
 
92
 
  thm″ : ∀ x → x ∙ ε ≈ x
93
 
  thm″ = {!!}
94
 
 
95
 
  -- agda2-goal-and-context:
96
 
 
97
 
  -- rm : RawMonoid″ (List Bool)
98
 
  -- ---------------------------
99
 
  -- Goal: (x : List Bool) →
100
 
  --       RawMonoid″._≈_ rm (RawMonoid″._∙_ rm x (RawMonoid″.ε rm)) x
101
 
 
102
 
module M₁ (Z : Set₁) where
103
 
 
104
 
  postulate
105
 
    P : Set
106
 
    Q : Set → Set
107
 
 
108
 
module M₂ (X Y : Set) where
109
 
 
110
 
  module M₁′ = M₁ Set
111
 
  open M₁′
112
 
 
113
 
  p : P
114
 
  p = {!!}
115
 
 
116
 
  q : Q X
117
 
  q = {!!}
118
 
 
119
 
postulate X : Set
120
 
 
121
 
pp : M₂.M₁′.P X X
122
 
pp = {!!}
 
 
b'\\ No newline at end of file'