search

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

Sequent is modified by auto-prove #80

Closed olaure01 closed 3 years ago

olaure01 commented 3 years ago

For ⊢ A⊗B, A^⅋B^, click on ⅋ then double click on ⊢, turns ⊢ A⊗B, A^, B^ into ⊢ A^, A⊗B, B^.

olaure01 commented 3 years ago

After some thought, the best is maybe to always display the "post-exchange" conclusion. It will solve the problem above and only impact the conclusion of tensor rules for which it could even be more natural.

etiennecallies commented 3 years ago

I was not sure what you wanted this morning so I chose to display only post-exchange sequent.

  1. It's simpler to implement.
  2. It displays exactly what you would see if you proved the sequent by yourself.
olaure01 commented 3 years ago

Sorry "post" depends on the direction... I meant display the lower part of the exchange rule, at least for the final sequent, and probably more readable (closer to usual paper writing) if applied to all rules.

etiennecallies commented 3 years ago

It needs a few adaptations in javascript but it should not be long.

etiennecallies commented 3 years ago

Fixed by c542aaf