search

alcides / aeon

Aeon programming language
https://alcides.github.io/aeon/
8 stars 3 forks source link

Push implications inward in type checking. #15

Closed alcides closed 6 months ago

alcides commented 11 months ago

Liquid Type checking currently obtains the VCs from the leafs upward to the root.

The idea of this issue is to push the binders inward to the leafs of the VCs, so we can get more localized error messages.

alcides commented 6 months ago

For the moment, this idea is shutdown as VCs can generate multiple calls to the SMT solver in Horn Clauses.