search

dselsam / binport

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

error: invalid argument name 'self' #24

Closed dselsam closed 3 years ago

dselsam commented 3 years ago 
import Mathlib.data.rat.basic
#check (1 : ℚ).num -- error: invalid argument name 'self' for function 'Mathlib.rat.num'

I have not been able to reproduce this without importing mathlib.

gebner commented 3 years ago

This looks like Lean 4 desugars x.num to rat.num (self := x). And Lean 3 uses a different name for the argument.

dselsam commented 3 years ago

Apparently it only desugars to self if the function (in this case rat.num) is registered as a projection. This is why the error cannot be reproduced without abstraction-breaking code that registers projections.

dselsam commented 3 years ago

@gebner What if we just backport the name-change? https://github.com/leanprover-community/lean/blob/master/src/frontends/lean/structure_cmd.cpp#L1248

gebner commented 3 years ago

Backport sounds good to me.