search

leanprover-community / mathport

Mathport is a tool for porting Lean3 projects to Lean4
Apache License 2.0
43 stars 15 forks source link

feat: smart naming for theorems #219

Closed rwbarton closed 1 year ago

rwbarton commented 1 year ago

For each theorem, use the alignments for names appearing in the type of the theorem to make a smart guess for the Lean 4 translated name.

rwbarton commented 1 year ago

Output can be inspected at https://github.com/leanprover-community/mathport/releases/tag/pr-smart-naming-9e81f5e