Closed olaure01 closed 3 years ago
Can be tested on preprod (click on LaTeX button)
A few suggestions:
LaTeX
Proof Drawing
button. You will then be able to select among: LaTeX source, PDF export, PNG image, Ascii or UTF8 representation."explicit exchange (i) (o-)
with help over (i)
:
either a short "Draw explicit exchange rules"
or some "Learn about explicit exchange option` and then open a window by clicking with "By default, no exchange rule will appear in the export: the output will be displayed as in the interface (snapshot). With explicit exchange activated, required exchanges will appear in the export, to get derivation rules applied strictly through the proof."Good suggestions, deployed on preprod.
To avoid conflicts it's easier for me to merge. I would be happy to improve the export popup later on.
OCaml side only. Interface is missing.