← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/Induction/Lexicographic.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/Lexicographic.agda
65
65
  -- The Ackermann function à la Rózsa Péter.
66
66
 
67
67
  ackermann : ℕ → ℕ → ℕ
68
 
  ackermann m n = build [ N.rec-builder ⊗ N.rec-builder ]
69
 
                        AckPred ack (m , n)
70
 
    where
71
 
    AckPred : ℕ × ℕ → Set
72
 
    AckPred _ = ℕ
73
 
 
74
 
    ack : ∀ p → (N.Rec ⊗ N.Rec) AckPred p → AckPred p
75
 
    ack (zero  , n)     _                   = 1 + n
76
 
    ack (suc m , zero)  (_         , ackm•) = ackm• 1
77
 
    ack (suc m , suc n) (ack[1+m]n , ackm•) = ackm• ack[1+m]n
 
68
  ackermann m n =
 
69
    build [ N.rec-builder ⊗ N.rec-builder ]
 
70
          (λ _ → ℕ)
 
71
          (λ { (zero  , n)     _                   → 1 + n
 
72
             ; (suc m , zero)  (_         , ackm•) → ackm• 1
 
73
             ; (suc m , suc n) (ack[1+m]n , ackm•) → ackm• ack[1+m]n
 
74
             })
 
75
          (m , n)