96f9ee2a41
This PR ensures info tree users such as linters and request handlers have access to info subtrees created by async elab task by introducing API to leave holes filled by such tasks. **Breaking change**: other metaprogramming users of `Command.State.infoState` may need to call `InfoState.substituteLazy` on it manually to fill all holes.
85 lines
5.3 KiB
Text
85 lines
5.3 KiB
Text
[Elab.info]
|
||
• command @ ⟨6, 0⟩-⟨6, 31⟩ @ Lean.Elab.Command.elabSetOption
|
||
• [.] (Command.set_option "set_option" `trace.Elab.info []) @ ⟨6, 0⟩-⟨6, 26⟩
|
||
• option trace.Elab.info @ ⟨6, 11⟩-⟨6, 26⟩
|
||
1018unknowMVarIssue.lean:9:18-9:19: error: don't know how to synthesize placeholder
|
||
context:
|
||
α✝ β : Type
|
||
x : Fam2 α✝ β
|
||
α : Type
|
||
a : α
|
||
⊢ α
|
||
[Elab.info]
|
||
• command @ ⟨7, 0⟩-⟨10, 19⟩ @ Lean.Elab.Command.elabDeclaration
|
||
• α : Type @ ⟨7, 13⟩-⟨7, 14⟩ @ Lean.Elab.Term.elabIdent
|
||
• [.] α : some Sort.{?_uniq} @ ⟨7, 13⟩-⟨7, 14⟩
|
||
• α : Type @ ⟨7, 13⟩-⟨7, 14⟩
|
||
• a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩
|
||
• Fam2 α β : Type 1 @ ⟨7, 21⟩-⟨7, 29⟩ @ Lean.Elab.Term.elabApp
|
||
• [.] Fam2 : some Sort.{?_uniq} @ ⟨7, 21⟩-⟨7, 25⟩
|
||
• Fam2 : Type → Type → Type 1 @ ⟨7, 21⟩-⟨7, 25⟩
|
||
• α : Type @ ⟨7, 26⟩-⟨7, 27⟩ @ Lean.Elab.Term.elabIdent
|
||
• [.] α : some Type @ ⟨7, 26⟩-⟨7, 27⟩
|
||
• α : Type @ ⟨7, 26⟩-⟨7, 27⟩
|
||
• β : Type @ ⟨7, 28⟩-⟨7, 29⟩ @ Lean.Elab.Term.elabIdent
|
||
• [.] β : some Type @ ⟨7, 28⟩-⟨7, 29⟩
|
||
• β : Type @ ⟨7, 28⟩-⟨7, 29⟩
|
||
• x (isBinder := true) : Fam2 α β @ ⟨7, 17⟩-⟨7, 18⟩
|
||
• β : Type @ ⟨7, 33⟩-⟨7, 34⟩ @ Lean.Elab.Term.elabIdent
|
||
• [.] β : some Sort.{?_uniq} @ ⟨7, 33⟩-⟨7, 34⟩
|
||
• β : Type @ ⟨7, 33⟩-⟨7, 34⟩
|
||
• CustomInfo(Lean.Elab.InlayHint)
|
||
• _example (isBinder := true) : {α β : Type} → α → Fam2 α β → β @ ⟨7, 0⟩†!-⟨7, 7⟩†!
|
||
• a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩
|
||
• x (isBinder := true) : Fam2 α β @ ⟨7, 17⟩-⟨7, 18⟩
|
||
• CustomInfo(Lean.Elab.Term.BodyInfo)
|
||
• Partial term @ ⟨8, 2⟩-⟨10, 19⟩ @ Lean.Elab.Term.Quotation.elabMatchSyntax
|
||
• match α, β, x, a with
|
||
| α_1, .(α_1), Fam2.any, a => ?m x α_1 a
|
||
| .(Nat), .(Nat), Fam2.nat n, a => n : β @ ⟨8, 2⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabMatch
|
||
• x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩ @ Lean.Elab.Term.elabIdent
|
||
• [.] x : none @ ⟨8, 8⟩-⟨8, 9⟩
|
||
• x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩
|
||
• x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩ @ Lean.Elab.Term.elabIdent
|
||
• [.] x : none @ ⟨8, 8⟩-⟨8, 9⟩
|
||
• x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩
|
||
• [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
|
||
• [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
|
||
• @Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩
|
||
• [.] Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
|
||
• Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
|
||
• [.] n : none @ ⟨10, 13⟩-⟨10, 14⟩
|
||
• [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
|
||
• [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
|
||
• @Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩
|
||
• [.] a : none @ ⟨8, 2⟩†-⟨10, 19⟩†
|
||
• [.] Fam2.any : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) @ ⟨9, 4⟩-⟨9, 12⟩
|
||
• [.] a : some [mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]] @ ⟨8, 2⟩†-⟨10, 19⟩†
|
||
• α (isBinder := true) : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
|
||
• α : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
|
||
• Fam2.any : Fam2 α α @ ⟨9, 4⟩†-⟨9, 12⟩†
|
||
• α : Type @ ⟨9, 4⟩†-⟨9, 12⟩†
|
||
• a (isBinder := true) : α @ ⟨8, 2⟩†-⟨10, 19⟩†
|
||
• FVarAlias a: _uniq.592 -> _uniq.319
|
||
• FVarAlias α: _uniq.591 -> _uniq.317
|
||
• ?m x α a : α @ ⟨9, 18⟩-⟨9, 19⟩ @ Lean.Elab.Term.elabHole
|
||
• [.] Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
|
||
• Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
|
||
• [.] n : none @ ⟨10, 13⟩-⟨10, 14⟩
|
||
• [.] a : none @ ⟨8, 2⟩†-⟨10, 19⟩†
|
||
• [.] Fam2.nat : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) @ ⟨10, 4⟩-⟨10, 12⟩
|
||
• [.] n : some Nat @ ⟨10, 13⟩-⟨10, 14⟩
|
||
• [.] a : some [mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]] @ ⟨8, 2⟩†-⟨10, 19⟩†
|
||
• Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
|
||
• Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
|
||
• Fam2.nat n : Fam2 Nat Nat @ ⟨10, 4⟩†-⟨10, 14⟩
|
||
• n (isBinder := true) : Nat @ ⟨10, 13⟩-⟨10, 14⟩
|
||
• a (isBinder := true) : Nat @ ⟨8, 2⟩†-⟨10, 19⟩†
|
||
• FVarAlias a: _uniq.623 -> _uniq.319
|
||
• FVarAlias n: _uniq.622 -> _uniq.317
|
||
• n : Nat @ ⟨10, 18⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabIdent
|
||
• [.] n : some Nat @ ⟨10, 18⟩-⟨10, 19⟩
|
||
• n : Nat @ ⟨10, 18⟩-⟨10, 19⟩
|
||
• @_example (isBinder := true) : {α β : Type} → α → Fam2 α β → β @ ⟨7, 0⟩-⟨7, 7⟩
|
||
[Elab.info]
|
||
• command @ ⟨11, 0⟩-⟨11, 0⟩ @ Lean.Elab.Command.elabEoi
|