Closed robblanco closed 7 years ago
Partially addresses #86. Term.norm is not used anywhere in the Abella codebase, its effects can be replicated by the standard observe-hnorm pattern, and it can produce invalid term structures: it is therefore removed. All tests pass.
Partially addresses #86. Term.norm is not used anywhere in the Abella codebase, its effects can be replicated by the standard observe-hnorm pattern, and it can produce invalid term structures: it is therefore removed. All tests pass.