Closed developedby closed 1 month ago
Previously, when reaching an unreachable case in a Mat term, the type checker would simply skip checking it.
This lead to the metas inside of that case never being filled, since they were not checked.
Now, we substitute all Met terms in unreachable cases with (Hol "unreachable")
Previously, when reaching an unreachable case in a Mat term, the type checker would simply skip checking it.
This lead to the metas inside of that case never being filled, since they were not checked.
Now, we substitute all Met terms in unreachable cases with (Hol "unreachable")