Closed agureev closed 1 year ago
Gets rid of hom-cod function and hence gets rid of unnecessary pattern matching during term annotation for function application. Alongside that, adds a case for checking well-definedness.
hom-cod
Gets rid of
hom-cod
function and hence gets rid of unnecessary pattern matching during term annotation for function application. Alongside that, adds a case for checking well-definedness.