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

[Coq] utf8 notations in Coq export #98

Closed olaure01 closed 3 years ago

olaure01 commented 3 years ago

Experimental notations in Coq for readability of proof script executions.

olaure01 commented 3 years ago

@etiennecallies Could we have it in pre-prod to see how it behaves? and I would be happy to have comments on your side about whether it is useful or not. If everything works as planned, removing the line Import LLNotations. in the Coq file should give exactly the same behavior as before (for users who prefer it).

etiennecallies commented 3 years ago

I can deploy it on preprod as soon as the PR https://github.com/etiennecallies/click-and-collect/pull/99 is merged.

etiennecallies commented 3 years ago

Deployed on preprod. For the moment I don't see the difference...

olaure01 commented 3 years ago

When you execute a proof step by step, you should see the current goal written with utf8 notations rather than pure Coq ascii.

olaure01 commented 3 years ago

I am trying to avoid the explicit %nat in the Coq export but failing so far (see coq/coq#14305).