Closed vlopezj closed 7 years ago
When type-checking a Π-type, the domain is instantiated with the type of the codomain. Instead, the context should be extended, like in the λ case.
When type-checking a Π-type, the domain is instantiated with the type of the codomain. Instead, the context should be extended, like in the λ case.