option -O - Githubissues

Deducteam / isabelle_dedukti

Isabelle component generating Dedukti proofs

Other

3 stars 4 forks source link

Closed fblanqui closed 1 year ago

fblanqui commented 2 years ago

Currently, the command isabelle dedukti_generate takes as argument -O main.lp or -O main.dk but no file main.lp or main.dk are generated. This should be replaced by a single option -lp (default being dk output).
In README.md, references to isabelle dedukti_import should be removed.
In src/tools.scala, Tools should be removed and Tools2 renamed into Tools.

fblanqui commented 1 year ago

These issues seem deprecated with #16.