Inequivalence clause are not stored in the pool (mantis #51)

rlepigre / pml

New version of the PML language and (classical) proof assistant

http://pml-lang.org

MIT License

20 stars 2 forks source link

Inequivalence clause are not stored in the pool (mantis #51) #3

Closed craff closed 6 years ago

craff commented 6 years ago

Will only be useful when assuming inequivalence, which is not really possible currently.

Probably useless ... wait for a use case.

craff commented 6 years ago

A minimal piece of code has been added, as it is now used by one example. The current solution is not complete nor very efficient, but seems to suffice in practice:

This solution is to store inequalities in a list and re-test them at each add_equiv. In principle, it should also be tested when we learn than something is a no box value.