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
[Parsing] Make multiplicative connectives more associative than additive ones #173
Open
olaure01 opened 2 years ago
A * B + A * C
is parsed as((A ⊗ B) ⊕ A) ⊗ C
while(A ⊗ B) ⊕ (A ⊗ C)
would be more natural.