search

JetBrains / Arend

The Arend Proof Assistant
https://arend-lang.github.io/
Apache License 2.0
690 stars 33 forks source link

Introduce expression minimizer #307

Closed knisht closed 3 years ago

knisht commented 3 years ago

This PR aims to add a new kind of pretty printer -- expression minimizer. Minimizer can be used to convert core expressions to concrete with as little additional information as possible (by "additional information" I mean everything that can be hidden with PrettyPrinterConfig flags). Unfortunately, it is not stable at all, and it works without problems for very simple expressions. Yet I think it can be used with care in production.

knisht commented 3 years ago

For ease of code review, it is separated from #308