Equations
- Lean.Widget.instInhabitedInfoWithCtx = { default := { ctx := default, info := default } }
Equations
- Lean.Widget.Lean.Widget.InfoWithCtx.instRpcEncodingWithRpcRefInfoWithCtxRpcRef = { rpcEncode := fun {m} [Monad m] [Lean.Server.MonadRpcSession m] => [anonymous], rpcDecode := fun {m} [Monad m] [Lean.Server.MonadRpcSession m] => [anonymous] }
Equations
- Lean.Widget.instInhabitedCodeToken = { default := { info := default } }
Equations
- Lean.Widget.Lean.Widget.CodeToken.instRpcEncodingCodeTokenRpcEncodingPacket = { rpcEncode := fun {m} [Monad m] [Lean.Server.MonadRpcSession m] a => do let a ← Lean.Server.rpcEncode a.info pure { info := a }, rpcDecode := fun {m} [Monad m] [Lean.Server.MonadRpcSession m] a => do let a ← Lean.Server.rpcDecode a.info pure { info := a } }
@[inline]
Equations
Equations
- Lean.Widget.traverse e addr = (fun tritsLE go => do let e ← Lean.Meta.instantiateMVars e let a ← Lean.getLCtx go (List.drop 1 (tritsLE [] addr)) a e) Lean.Widget.traverse.tritsLE Lean.Widget.traverse.go
def
Lean.Widget.formatInfos
(e : Lean.Expr)
:
Lean.MetaM (Lean.Format × Std.RBMap Nat Lean.Elab.Info compare)
Equations
def
Lean.Widget.formatExplicitInfos
(e : Lean.Expr)
:
Lean.MetaM (Lean.Format × Std.RBMap Nat Lean.Elab.Info compare)
Equations
- Lean.Widget.formatExplicitInfos e = let optsPerPos := Std.RBMap.ofList [(1, Lean.KVMap.setBool Lean.KVMap.empty `pp.all true)]; Lean.Widget.formatWithOpts e optsPerPos
def
Lean.Widget.tagExprInfos
(ctx : Lean.Elab.ContextInfo)
(infos : Std.RBMap Nat Lean.Elab.Info compare)
(tt : Lean.Widget.TaggedText (Nat × Nat))
:
Equations
- Lean.Widget.tagExprInfos ctx infos tt = (fun go => go tt) (Lean.Widget.tagExprInfos.go ctx infos)
partial def
Lean.Widget.tagExprInfos.go
(ctx : Lean.Elab.ContextInfo)
(infos : Std.RBMap Nat Lean.Elab.Info compare)
(tt : Lean.Widget.TaggedText (Nat × Nat))
:
Equations
- Lean.Widget.exprToInteractive e = do let discr ← Lean.Widget.formatInfos e let x : Lean.Format × Std.RBMap Nat Lean.Elab.Info compare := discr match x with | (fmt, infos) => let tt := Lean.Widget.TaggedText.prettyTagged fmt 0; do let a ← Lean.getEnv let a_1 ← Lean.getMCtx let a_2 ← Lean.getOptions let a_3 ← Lean.getCurrNamespace let a_4 ← Lean.getOpenDecls let ctx : Lean.Elab.ContextInfo := { env := a, fileMap := default, mctx := a_1, options := a_2, currNamespace := a_3, openDecls := a_4 } pure (Lean.Widget.tagExprInfos ctx infos tt)
Equations
- Lean.Widget.exprToInteractiveExplicit e = do let discr ← Lean.Widget.formatExplicitInfos e let x : Lean.Format × Std.RBMap Nat Lean.Elab.Info compare := discr match x with | (fmt, infos) => let tt := Lean.Widget.TaggedText.prettyTagged fmt 0; do let a ← Lean.getEnv let a_1 ← Lean.getMCtx let a_2 ← Lean.getOptions let a_3 ← Lean.getCurrNamespace let a_4 ← Lean.getOpenDecls let ctx : Lean.Elab.ContextInfo := { env := a, fileMap := default, mctx := a_1, options := a_2, currNamespace := a_3, openDecls := a_4 } let infos : Std.RBMap Nat Lean.Elab.Info compare := Std.RBMap.erase infos 1 pure (Lean.Widget.tagExprInfos ctx infos tt)