search

advancedresearch / poi

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

Remove `eqb => eq` #1062

Open bvssvni opened 3 years ago

bvssvni commented 3 years ago

An alternative to adding a context solver is separating eqb and eq. This means eqb => eq must be removed. However, eq{(: bool), (: bool)} might be used instead.

bvssvni commented 3 years ago

Could add eqb <=> eq{(: bool), (: bool)}.

This can be used as following to lift eq into eqb:

(a & b = c) <=> eq{(: bool), (: bool)}(a & b)(c)

bvssvni commented 3 years ago

One idea is to use <-> for eqb.