lambdapi icon indicating copy to clipboard operation
lambdapi copied to clipboard
verified publisher icon Deducteam

Add export to Lean

Open fblanqui opened this issue 1 year ago • 0 comments

TODO:

  • [x] factorize the beginning of coq.ml and lean.ml into stt.ml
  • [x] update doc
  • [ ] in Lean.print: prefix namespace by root_path

fblanqui avatar Feb 12 '25 20:02 fblanqui