Add `(!= _)` constraint on constants in rules - Githubissues

advancedresearch / poi

a pragmatic point-free theorem prover assistant

Apache License 2.0

136 stars 7 forks source link

Add `(!= _)` constraint on constants in rules #1095

Open bvssvni opened 9 months ago

bvssvni commented 9 months ago

Currently, this is not possible to express.

Add:

[ ] inv((* \k:(!= 0))) => (/ k)
[ ] inv((/ \k:(!= 0))) => (* k)