;;
;; 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 {[]}]
           [_ {}]}]})]}))

(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 $Char
  (type
    {[$var-match (lambda [$tgt] {tgt})]
     [$inductive-match
      (destructor
        {[,$c []
          {[$tgt (if (= tgt c)
                     {[]}
                     {})]}]})]
     [$= eq-c?]}))

(define $String
  (type
    {[$var-match (lambda [$tgt] {tgt})]
     [$= eq-s?]}))

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