ComputerAidedLL / click-and-collect

A web interactive tool for building proofs in the sequent calculus of Linear Logic, with its backend written in OCaml
GNU Lesser General Public License v2.1
17 stars 2 forks source link

Proof transformation: double click on reversible formula #163

Open etiennecallies opened 3 years ago

etiennecallies commented 3 years ago

Double click reverses hereditarily the reversible sub-formulas? Dedicated button for full reversing of all concluding reversible formulas (including reversible sub-formulas)? https://github.com/etiennecallies/click-and-collect/pull/158#issuecomment-882074577

Trying to reverse a ! with not a ?-context generates an error message Can not apply 'promotion' rule: the context must contain formulas starting by '?' only. It is OK, but just to mention that an alternative would be not to activate reversibility of ! in such a situation. Not sure what is the best to do. https://github.com/etiennecallies/click-and-collect/pull/158#issuecomment-882075044