;; ;; Base.egi ;; (define $Something (type {[$var-match (lambda [$tgt] {tgt})]})) (define $Bool (type {[$var-match (lambda [$tgt] {tgt})] [$inductive-match (destructor {[true [] {[ {[]}] [#t {[]}] [_ {}]}] [false [] {[ {[]}] [#f {[]}] [_ {}]}]})] [$= (lambda [$val $tgt] (match [val tgt] [Bool Bool] {[[ ] #t] [[ #t] #t] [[#t ] #t] [[ ] #t] [[ #f] #t] [[#f ] #t] [[_ _] ]}))]})) (define $or (lambda [$b1 $b2] (match b1 Bool {[ #t] [ b2]}))) (define $and (lambda [$b1 $b2] (match b1 Bool {[ b2] [ #f]}))) (define $not (lambda [$b] (match b Bool {[ #f] [ #t]}))) (define $Order (type {[$var-match (lambda [$tgt] {tgt})] [$inductive-match (destructor {[less [] {[ {[]}] [_ {}]}] [equal [] {[ {[]}] [_ {}]}] [greater [] {[ {[]}] [_ {}]}]})] [$= (lambda [$val $tgt] (match [val tgt] [Order Order] {[[ ] #t] [[ ] #t] [[ ] #t] [[_ _] #f]}))]}))