number.egi

(define $Integer
  (type
    {[$var-match (lambda [$tgt] {tgt})]
     [$inductive-match
      (destructor
        {[,$n []
          {[$tgt (if (= tgt n)
                     {[]}
                     {})]}]})]
     [$= (lambda [$val $tgt] (eq-n? val tgt))]}))

(define $compare-integer
  (lambda [$m $n]
    (if (lt-n? m n)
        <less>
        (if (eq-n? m n)
            <equal>
            <greater>))))

(define $Double
  (type
    {[$var-match (lambda [$tgt] {tgt})]
     [$inductive-match
      (destructor
        {[,$d []
          {[$tgt (if (= tgt d)
                     {[]}
                     {})]}]})]
     [$= (lambda [$val $tgt] (eq-f? val tgt))]}))

(define $compare-float
  (lambda [$d1 $d2]
    (if (lt-f? d1 d2)
        <less>
        (if (eq-f? d1 d2)
            <equal>
            <greater>))))

(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)}]
                    [_ {}]})]}]})]
     [$= (lambda [$val $tgt] (eq-n? val tgt))]}))

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

(define $min
  (lambda [$ns]
    (match ns (List Integer)
      {[<cons $n <nil>> n]
       [<cons $n $rs>
        (let {[$r (min rs)]}
          (match (compare-integer n r) Order
            {[<less> n]
             [_ r]}))]})))

(define $max
  (lambda [$ns]
    (match ns (List Integer)
      {[<cons $n <nil>> n]
       [<cons $n $rs>
        (let {[$r (max rs)]}
          (match (compare-integer n r) Order
            {[<greater> n]
             [_ r]}))]})))

(define $min&max
  (lambda [$ns]
    (match ns (List Integer)
      {[<cons $n <nil>> [n n]]
       [<cons $n $rs>
        (let {[[$min-n $max-n] (min&max rs)]}
          (match (compare-integer n min-n) Order
            {[<less> [n max-n]]
             [_ (match (compare-integer n max-n) Order
                  {[<greater> [min-n n]]
                   [_ [min-n max-n]]})]}))]})))

(define $gcd
  (lambda [$ns]
    (match ns (Set Integer)
      {[<cons $n <nil>> n]
       [<cons (& ,(min ns) $m)
              $rs>
        (gcd {m @((remove-all Integer)
                    (map (lambda [$r] (mod r m))
                         rs)
                    0)})]})))