hermit-0.3.0.0: examples/evaluation/Eval.hss

load-as-rewrite "WWA" "WW-Ass-A.hss"
flatten-module
binding-of 'eval
ww-result-split [| abs |] [| rep |] (ww-result-AssA-to-AssC WWA)
{ def-rhs
  let-subst
  { let-body
    alpha-lam 'e
    lam-body
    unfold 'abs
  }
  { rhs-of 'work
    alpha-lam 'e ; lam-body
    unfold 'rep
    bash
    [lam-body, lam-body]
    { consider case ; [ case-alt 1, alt-rhs ] ; abstract 'm
      consider case ; [ case-alt 1, alt-rhs ] ; abstract 'n
    }
    any-bu (fold 'rep)
    any-td (forward ww-result-fusion)
  }
}