egison-1.1.0: etc/lib/number.egi

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

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

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

(define $between
  (lambda [$m $n]
    (match (compare-integer m n) Order
      {[<less> {m @(between (+ m 1) n)}]
       [<equal> {n}]})))