search

dselsam / binport

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

Auto-generated names need to depend on module #12

Closed dselsam closed 3 years ago

dselsam commented 3 years ago

There are currently auto-generated names in lean4 that do not depend on the module and so may clash across modules. A fix is implemented here: https://github.com/dselsam/lean4/commit/91e1f6cba9fa989ad1db9c2e5a6edf997f74f7eb

leodemoura commented 3 years ago

This is intentional. We generate concise names for notation based on their actual definition. We want to have concise names because we want to be able to use the name to selectively activate/deactivate notation in the future. The generated names can be easily guessed by users. Example:

infix:65 "+" => Nat.add
#check «term_+_»

Note that, we have scoped notation, and including the full module name will create problems for activating this kind of notation. I don't think this is an issue for people using Lean 4 directly. It is equivalent to getting an error because you wrote the same function in different files. The default solution is to use namespaces, and the same works here too.

dselsam commented 3 years ago

Whoops, I will update mathport to put the notation inside a namespace and revert the commit above.

dselsam commented 3 years ago

Closed by https://github.com/dselsam/mathport/commit/5bbca26e238b7db1aa71795f02a14cf88ca3b19f