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]
           [[<true> #t] #t]
           [[#t <true>] #t]
           [[<false> <false>] #t]
           [[<false> #f] #t]
           [[#f <false>] #t]
           [[_ _] <false>]}))]}))

(define $or
  (lambda [$b1 $b2]
    (match b1 Bool
      {[<true> #t]
       [<false> b2]})))

(define $and
  (lambda [$b1 $b2]
    (match b1 Bool
      {[<true> b2]
       [<false> #f]})))

(define $not
  (lambda [$b]
    (match b Bool
      {[<true> #f]
       [<false> #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]}))]}))