structure ProofWidgets.ExprPresenter : Type

An Expr presenter is similar to a delaborator but outputs HTML trees instead of syntax, and the output HTML can contain elements which interact with the original Expr in some way. We call interactive outputs with a reference to the original input presentations.

• userName : String

  A user-friendly name for this presenter. For example, "LaTeX".

• layoutKind : LayoutKind

  Whether the output HTML has inline (think something which fits in the space normally occupied by an Expr, e.g. LaTeX) or block (think large diagram which needs dedicated space) layout.

• present : Lean.Expr → Lean.MetaM Html

opaque ProofWidgets.exprPresenters : Lean.TagAttribute

Register an Expr presenter. It must have the type ProofWidgets.ExprPresenter.

@[implemented_by _private.ProofWidgets.Presentation.Expr.0.ProofWidgets.evalExprPresenterUnsafe]

opaque ProofWidgets.evalExprPresenter (env : Lean.Environment) (opts : Lean.Options) (constName : Lean.Name) : Except String ExprPresenter

structure ProofWidgets.GetExprPresentationsParams : Type

• expr : Lean.Server.WithRpcRef ExprWithCtx

instance ProofWidgets.instRpcEncodableGetExprPresentationsParams : Lean.Server.RpcEncodable GetExprPresentationsParams

Equations

• One or more equations did not get rendered due to their size.

structure ProofWidgets.ExprPresentationData : Type

• name : Lean.Name
• userName : String
• html : Html

instance ProofWidgets.instRpcEncodableExprPresentationData : Lean.Server.RpcEncodable ExprPresentationData

Equations

• ProofWidgets.instRpcEncodableExprPresentationData = { rpcEncode := ProofWidgets.instRpcEncodableExprPresentationData.enc✝, rpcDecode := ProofWidgets.instRpcEncodableExprPresentationData.dec✝ }

structure ProofWidgets.ExprPresentations : Type

• presentations : Array ExprPresentationData

instance ProofWidgets.instRpcEncodableExprPresentations : Lean.Server.RpcEncodable ExprPresentations

Equations

• ProofWidgets.instRpcEncodableExprPresentations = { rpcEncode := ProofWidgets.instRpcEncodableExprPresentations.enc✝, rpcDecode := ProofWidgets.instRpcEncodableExprPresentations.dec✝ }

def ProofWidgets.getExprPresentations : GetExprPresentationsParams → Lean.Server.RequestM (Lean.Server.RequestTask ExprPresentations)

Equations

• One or more equations did not get rendered due to their size.

def ProofWidgets.getExprPresentations.addPresenterIfApplicable (expr : ExprWithCtx) (nm : Lean.Name) (ps : Array ExprPresentationData) : Lean.Server.RequestM (Array ExprPresentationData)

Equations

• One or more equations did not get rendered due to their size.

structure ProofWidgets.GetExprPresentationParams : Type

• expr : Lean.Server.WithRpcRef ExprWithCtx
• name : Lean.Name

  Name of the presenter to use.

instance ProofWidgets.instRpcEncodableGetExprPresentationParams : Lean.Server.RpcEncodable GetExprPresentationParams

Equations

• One or more equations did not get rendered due to their size.

structure ProofWidgets.ExprPresentationProps : Type

• expr : Lean.Server.WithRpcRef ExprWithCtx

instance ProofWidgets.instRpcEncodableExprPresentationProps : Lean.Server.RpcEncodable ExprPresentationProps

Equations

• One or more equations did not get rendered due to their size.

def ProofWidgets.ExprPresentation : Component ExprPresentationProps

This component shows a selection of all known and applicable ProofWidgets.ExprPresenters which are used to render the expression when selected. The one with highest precedence (TODO) is shown by default.

Equations

• One or more equations did not get rendered due to their size.