search

Deducteam / lambdapi

Proof assistant based on the λΠ-calculus modulo rewriting
Other
280 stars 35 forks source link

Support for negative priorities #706

Closed gabrielhdt closed 7 months ago

gabrielhdt commented 3 years ago

See #664.

The Pratt parsing library https://forge.tedomum.net/koizel/pratter allows to use negative priorities for operators, but the parser doesn't allow to input negative floats,

notation o infix -3;

is not allowed.

gabrielhdt commented 7 months ago

Fixed by #1093.