search

dselsam / binport

A tool for building Lean4 .olean files from Lean3 export data
Apache License 2.0
10 stars 1 forks source link

Capitalization mismatch #23

Open dselsam opened 3 years ago

dselsam commented 3 years ago

Lean4 capitalization conventions have changed. For example, types are now capitalized, so set α would normally be written as Set α. These mismatches make using the auto-ported Mathlib libraries in Lean4 rather awkward. Also, when the Mathlib namespace is merely opened, MonadStateOf.set (exported into _root_ in Init) clashes with Mathlib.set and so the full name Mathlib.set must be written explicitly.

Both problems would be solved by having mathport automatically change the capitalization of the names as appropriate.

dselsam commented 3 years ago

Auto-capitalizing would introduce new problems though. If Mathlib.fin became Mathlib.Fin, then neither Fin would be usable outside of the Mathlib namespace. Having two Fins is already annoying though. Maybe auto-capitalization + more-alignments is the way to go.