← Back to branch summary

~ubuntu-branches/ubuntu/utopic/agda-stdlib/utopic-proposed

« back to all changes in this revision

Viewing changes to src/Induction.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 09:46:46 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805094646-zqd0c4m8ndngqg6x
Tags: 0.8-1
* [4ca6fd0] Update debian/watch to fetch tarballs from github
* [84d4313] Imported Upstream version 0.8
* [7b08243] debian/control: Require agda 2.4.x per upstream
* [37e7e10] debian/control: Standards-Version → 3.9.5, no changes required.
* [9051b9d] Run upstream's "GenerateEverything" script

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Induction.agda
19
19
-- A RecStruct describes the allowed structure of recursion. The
20
20
-- examples in Induction.Nat should explain what this is all about.
21
21
 
22
 
RecStruct : ∀ {a} → Set a → Set (suc a)
23
 
RecStruct {a} A = Pred A a → Pred A a
 
22
RecStruct : ∀ {a} → Set a → (ℓ₁ ℓ₂ : Level) → Set _
 
23
RecStruct A ℓ₁ ℓ₂ = Pred A ℓ₁ → Pred A ℓ₂
24
24
 
25
25
-- A recursor builder constructs an instance of a recursion structure
26
26
-- for a given input.
27
27
 
28
 
RecursorBuilder : ∀ {a} {A : Set a} → RecStruct A → Set _
 
28
RecursorBuilder : ∀ {a ℓ₁ ℓ₂} {A : Set a} → RecStruct A ℓ₁ ℓ₂ → Set _
29
29
RecursorBuilder Rec = ∀ P → Rec P ⊆′ P → Universal (Rec P)
30
30
 
31
31
-- A recursor can be used to actually compute/prove something useful.
32
32
 
33
 
Recursor : ∀ {a} {A : Set a} → RecStruct A → Set _
 
33
Recursor : ∀ {a ℓ₁ ℓ₂} {A : Set a} → RecStruct A ℓ₁ ℓ₂ → Set _
34
34
Recursor Rec = ∀ P → Rec P ⊆′ P → Universal P
35
35
 
36
36
-- And recursors can be constructed from recursor builders.
37
37
 
38
 
build : ∀ {a} {A : Set a} {Rec : RecStruct A} →
 
38
build : ∀ {a ℓ₁ ℓ₂} {A : Set a} {Rec : RecStruct A ℓ₁ ℓ₂} →
39
39
        RecursorBuilder Rec →
40
40
        Recursor Rec
41
41
build builder P f x = f x (builder P f x)
43
43
-- We can repeat the exercise above for subsets of the type we are
44
44
-- recursing over.
45
45
 
46
 
SubsetRecursorBuilder : ∀ {a ℓ} {A : Set a} →
47
 
                        Pred A ℓ → RecStruct A → Set _
 
46
SubsetRecursorBuilder : ∀ {a ℓ₁ ℓ₂ ℓ₃} {A : Set a} →
 
47
                        Pred A ℓ₁ → RecStruct A ℓ₂ ℓ₃ → Set _
48
48
SubsetRecursorBuilder Q Rec = ∀ P → Rec P ⊆′ P → Q ⊆′ Rec P
49
49
 
50
 
SubsetRecursor : ∀ {a ℓ} {A : Set a} →
51
 
                 Pred A ℓ → RecStruct A → Set _
 
50
SubsetRecursor : ∀ {a ℓ₁ ℓ₂ ℓ₃} {A : Set a} →
 
51
                 Pred A ℓ₁ → RecStruct A ℓ₂ ℓ₃ → Set _
52
52
SubsetRecursor Q Rec = ∀ P → Rec P ⊆′ P → Q ⊆′ P
53
53
 
54
 
subsetBuild : ∀ {a ℓ} {A : Set a} {Q : Pred A ℓ} {Rec : RecStruct A} →
 
54
subsetBuild : ∀ {a ℓ₁ ℓ₂ ℓ₃}
 
55
                {A : Set a} {Q : Pred A ℓ₁} {Rec : RecStruct A ℓ₂ ℓ₃} →
55
56
              SubsetRecursorBuilder Q Rec →
56
57
              SubsetRecursor Q Rec
57
58
subsetBuild builder P f x q = f x (builder P f x q)