egison-0.3.0.0: etc/lib/number.egi

(define $Number
  (type
    {[$var-match (lambda [$tgt] {tgt})]
     [$equal? (lambda [$val $tgt]
                (= val tgt))]}))

(define $Nat
  (type
    {[$var-match (lambda [$tgt] {tgt})]
     [$inductive-match
      (deconstructor
        {[o []
          {[0 {[]}]
           [_ {}]
           }]
         [s [Nat]
          {[$tgt (match (compare-number tgt 0) Order
                   {[<greater> {(- tgt 1)}]
                    [_ {}]})]
           }]
         })]
     [$equal? (lambda [$val $tgt]
                (= val tgt))]
     }))