search

leanprover / lean4

Lean 4 programming language and theorem prover
https://lean-lang.org
Apache License 2.0
4.46k stars 388 forks source link

variable-notation-variable chain breaks hygiene tracking #2535

Open Kha opened 11 months ago

Kha commented 11 months ago

From https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Notation.20introduces.20sorry/near/390699774:

variable (x : Nat)
local notation "Finx" => Fin x

def val (y : Finx) : Nat := y

variable (y : Finx)

-- Declaration uses sorry:
def val' : Nat := y

The issue is here: https://github.com/leanprover/lean4/blob/e9d60e143a8b1ee06be1f201f78068250a2b8949/src/Lean/Elab/Command.lean#L442-L449 We first elaborate all section variables as binders and then register them as such but that is wrong if one section variable references another via a notation, which is where sectionFVars is needed. We should elaborate and add them to sectionFVars one by one.

Kha commented 11 months ago

@leodemoura Is it safe to separate an elabBinders into nested invocations of elabBinder? I believe so because the only effect is that universeConstraintsCheckpoint is run multiple times. In that case I'm happy to implement the small fix.