search

dselsam / binport

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

Is idDelta still necessary? #10

Closed dselsam closed 3 years ago

dselsam commented 3 years ago

Currently, idDelta exists in Lean4, and the kernel has the same special support for it as in Lean3, except there is a capitalization mismatch:

https://github.com/leanprover/lean4/blob/master/src/Init/Prelude.lean#L26 https://github.com/leanprover/lean4/blob/master/src/kernel/type_checker.cpp#L817 https://github.com/leanprover/lean4/blob/master/src/kernel/type_checker.cpp#L1044

I eagerly fixed the mismatch on my branch when I was porting https://github.com/dselsam/lean4/commit/9f22bbb08f61f7a6c90747f97dfed42eb4de9eb7 but it is not clear if we still need the feature. I will see if we can port without it.

dselsam commented 3 years ago

Confirmed: we can auto-port mathlib without idDelta.

Kha commented 3 years ago

@leodemoura fyi, I was confused as to why I couldn't find any reference to idDelta. It's because the kernel code still uses id_delta (which of course doesn't matter right now because we never actually use it): https://github.com/leanprover/lean4/blob/master/src/kernel/type_checker.cpp#L1044-L1045

leodemoura commented 3 years ago

id_delta is a leftover from Lean 3. Daniel just sent me a message saying he doesn't need it for the porting tool. I will delete id_delta from the Lean 4 kernel, and idDelta from stdlib.