![]() Previously expected propositions were erased frequently (at lets and ifs) and checking for logical entailment was unidirectional instead of bidirectional. In other words, instead of checking if propositions held at the leaves of the AST, we would typecheck the AST and blindly propagate up ALL logical info we learned at each step. This meant that we would get exponential blow up of propositions even when we didn't care about their content. With this commit, instead now we send down expected types *and* propositions so we can verify expected types and propisitions are satisfied at leaves, thereby relieving the need to constantly report up huge amounts of logical info while typechecking. |
||
---|---|---|
.. | ||
typed | ||
typed-racket | ||
info.rkt | ||
LICENSE.txt |