base.egi

;;
;; Base.egi
;;

(define $Something (type {[$var-match (lambda [$tgt] {tgt})]}))

(define $Bool
  (type
    {[$var-match (lambda [$tgt] {tgt})]
     [$inductive-match
      (destructor
        {[true []
          {[<true> {[]}]
           [#t {[]}]
           [_ {}]}]
         [false []
          {[<false> {[]}]
           [#f {[]}]
           [_ {}]}]})]
     [$=
      (lambda [$val $tgt]
        (match [val tgt] [Bool Bool]
          {[[<true> <true>] #t]
           [[<false> <false>] #t]
           [[_ _] #f]}))]}))

(define $or
  (lambda [$b1 $b2]
    (if b1
        #t
        b2)))

(define $and
  (lambda [$b1 $b2]
    (if b1
        b2
        #f)))

(define $not
  (lambda [$b]
    (if b
        #f
        #t)))

(define $Order
  (type
    {[$var-match (lambda [$tgt] {tgt})]
     [$inductive-match
      (destructor
        {[less []
          {[<less> {[]}]
           [_ {}]}]
         [equal []
          {[<equal> {[]}]
           [_ {}]}]
         [greater []
          {[<greater> {[]}]
           [_ {}]}]})]
     [$=
      (lambda [$val $tgt]
        (match [val tgt] [Order Order]
          {[[<less> <less>] #t]
           [[<equal> <equal>] #t]
           [[<greater> <greater>] #t]
           [[_ _] #f]}))]}))