Auto-reverse selection rule in atomic context

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

19 stars 2 forks source link

Auto-reverse selection rule in atomic context #64

Open olaure01 opened 3 years ago

olaure01 commented 3 years ago

Add the following auto-reverse rule: ?A with context with Zero, Dual and Litt only maps to A, ?A with same context (i.e. apply contraction and dereliction) if not of the shape X, X^, ?A.

etiennecallies commented 3 years ago

Is it an expected behavior? Should we ignore selection when there is already the formula without whynot? https://user-images.githubusercontent.com/7634514/116568410-bf584e00-a908-11eb-88ad-0efe2511ba6d.mp4

olaure01 commented 3 years ago

Not really expected... multiple actions on the auto-reverse button neither... Indeed checking the immediate sub-formula is not already there is nice, but would not solve the case of ?(X|(Y&Z)),X,Y for example.