← Back to branch summary

~ubuntu-branches/ubuntu/raring/agda-stdlib/raring

« back to all changes in this revision

Viewing changes to src/Induction/Nat.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2013-04-10 10:30:20 UTC
  • mfrom: (2.1.7 experimental)
  • Revision ID: package-import@ubuntu.com-20130410103020-bcspfz3whyy5iafu
Tags: 0.7-1
* [6d52289] Imported Upstream version 0.7
* [54104d0] Update Depends and Build-Depends for this version, compatible
  with Agda 2.3.2
* [b3ddce4] No need for the .install file to be executable (thanks lintian)
* [a9a6cb7] Standards-Version → 3.9.4, no changes required

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Induction/Nat.agda
90
90
 
91
91
  -- The half function.
92
92
 
93
 
  HalfPred : ℕ → Set
94
 
  HalfPred _ = ℕ
95
 
 
96
93
  half₁ : ℕ → ℕ
97
 
  half₁ = cRec HalfPred half₁'
98
 
    where
99
 
    half₁' : ∀ n → CRec HalfPred n → HalfPred n
100
 
    half₁' zero          _                = zero
101
 
    half₁' (suc zero)    _                = zero
102
 
    half₁' (suc (suc n)) (_ , half₁n , _) = suc half₁n
 
94
  half₁ = cRec _ λ
 
95
    { zero          _                → zero
 
96
    ; (suc zero)    _                → zero
 
97
    ; (suc (suc n)) (_ , half₁n , _) → suc half₁n
 
98
    }
103
99
 
104
100
  half₂ : ℕ → ℕ
105
 
  half₂ = <-rec HalfPred half₂'
106
 
    where
107
 
    half₂' : ∀ n → <-Rec HalfPred n → HalfPred n
108
 
    half₂' zero          _   = zero
109
 
    half₂' (suc zero)    _   = zero
110
 
    half₂' (suc (suc n)) rec = suc (rec n (≤′-step ≤′-refl))
 
101
  half₂ = <-rec _ λ
 
102
    { zero          _   → zero
 
103
    ; (suc zero)    _   → zero
 
104
    ; (suc (suc n)) rec → suc (rec n (≤′-step ≤′-refl))
 
105
    }