Library number.egi

In the library lib/number.egi, the Integer type, the Double type, and Nat type are defined.

Type : Integer

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

This type is useful to deal with integer.

Type : Double

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

This type is useful to deal with float number.

Type : Nat

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

This type is useful to deal with natural number.

      
(define $fib
  (lambda [$n]
    (match n Nat
      {[<o> 1]
       [<s <o>> 1]
       [<s <s $n1>> (+ (fib (+ n1 1)) (fib n1))]})))