epfl-lara / lisa

Proof assistant based on first-order logic and set theory
Apache License 2.0
33 stars 18 forks source link

Printer and Parser should allow unicode aliases for symbols #75

Closed SimonGuilloud closed 1 year ago

SimonGuilloud commented 1 year ago

The parser and printer should be able to use alternate names for symbols. For solidity and encapsulation, it should take a (bijective) map as argument. In the simplest case, this can be just printing m(id) instead of id, and parsing to m-1(token).

Bonus feature would be to allow to specify prefix or infix on top of an alias.