LocalContext fields?

Stream: lean4

[Thomas Murrills]

I was wondering how the fields of LocalContext—fvarIdToDecl and decls—were related.

My guess would be that decls is semi-redundant with fvarIdToDecl, but keeps track of the order given that it's an array—that is, the list of values of lctx.fvarIdToDecl should be exactly the same as lctx.decls.reduceOption.toList up to order. (My second guess would be that decls potentially holds only a subset of the values in fvarIdToDecl.)

In this view, I'd also expect that each assignment in fvarIdToDecl : PersistentHashMap FVarId LocalDecl is of the form fvarId0 ↦ cdecl _ fvarId0 .. or fvarId0 ↦ ldecl _ fvarId0 ..—that is, each fvarId is assigned to an l- or cdecl which holds the same fvarId. I'd also expect it to be the case that the index is always the position in lctx.decls.reduceOption.

Is this indeed how it works? Context: I want to compare LocalContexts, and want to know if I can rely on these coincidences so that I can make fewer component comparisons. :)

[Jannis Limperg]

Afaiu fvarIdToDecl is just a cache for decls (allowing efficient lookup by FVarId). So your invariants should hold.