search

agda / agda

Agda is a dependently typed programming language / interactive theorem prover.
https://wiki.portal.chalmers.se/agda/pmwiki.php
Other
2.4k stars 339 forks source link

Draft: Add let expressions to internal syntax #7253

Open jespercockx opened 1 month ago

jespercockx commented 1 month ago

Currently there is no way to preserve let-bindings in the internal syntax, which is bad because it destroys sharing and prevents us from pretty-printing terms as the user wrote them. The goal of this PR is to work towards fixing that.