Closed pigworker closed 3 years ago
We're now typechecking the propositions which show up as goals and hypotheses. Admittedly, there are only two types just now: Type and Prop. But even that lets us diagnose nonsense much earlier and deliver a less zen UX.
Type
Prop
We're now typechecking the propositions which show up as goals and hypotheses. Admittedly, there are only two types just now:
TypeandProp. But even that lets us diagnose nonsense much earlier and deliver a less zen UX.