search

advancedresearch / poi

a pragmatic point-free theorem prover assistant
Apache License 2.0
137 stars 7 forks source link

Add support for custom symbols #915

Closed bvssvni closed 3 years ago

bvssvni commented 3 years ago

Currently, all symbols are hard-coded in the Symbol enum.

A symbol differs from a variable in how rules are matched against expressions. A variable matches against any sub-expression, while a symbol matches only against itself.

bvssvni commented 3 years ago

One idea is to parse everything as custom symbols which starts with two lowercase alphabetic letters.

bvssvni commented 3 years ago

Implemented. Closing.