Module eval

Evaluation, quoting, and conversion/equality checking

At a high level, this module implements three operations:

• eval : syntax -> value (Evaluator::eval_tm, Evaluator::eval_ty)
• quote : value -> syntax (Evaluator::quote_tm, Evaluator::quote_neu, Evaluator::quote_ty)
• convertable? : value -> value -> bool (Evaluator::equal_tm, Evaluator::element_of, Evaluator::subtype)

Structs

Evaluator

The context used in evaluation, quoting, and conversion checking