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

Add cut front and back #108

Closed etiennecallies closed 3 years ago

etiennecallies commented 3 years ago

@olaure01 I saw you had different ideas for Coq and Cut_proof.

Except Coq export, everything should work on preprod: https://linearon.modusponens.dev/

olaure01 commented 3 years ago

@etiennecallies I started implementing what is described in the enhancement proposal but I need more time. I will try to push quickly a direct preliminary version (with only the axiomatic approach) for defining and testing the export.

olaure01 commented 3 years ago

First test remarks:

etiennecallies commented 3 years ago

First test remarks:

  • in the pop-up window for cut formula: accept "Enter" to send the formula (currently it is necessary to click on Cut)

Done

  • in the pop-up window for cut formula: clear history from one call to the next

I made auto-selection on previously submitted cut formula, so that you can type new one or modify previous one.

  • add the cut rule in the list of derivation rules

Yes, done.

etiennecallies commented 3 years ago

@etiennecallies I started implementing what is described in the enhancement proposal but I need more time. I will try to push quickly a direct preliminary version (with only the axiomatic approach) for defining and testing the export.

No problem.

etiennecallies commented 3 years ago

Many thanks @olaure01 ! For me this is ready for merging.

olaure01 commented 3 years ago

Fixes #12