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 : ProofWidgets.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 ProofWidgets.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 ProofWidgets.ExprPresenter

structure ProofWidgets.GetExprPresentationsParams : Type

• expr : Lean.Server.WithRpcRef ProofWidgets.ExprWithCtx

instance ProofWidgets.instRpcEncodableGetExprPresentationsParams : Lean.Server.RpcEncodable ProofWidgets.GetExprPresentationsParams

Equations

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

structure ProofWidgets.ExprPresentationData : Type

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

instance ProofWidgets.instRpcEncodableExprPresentationData : Lean.Server.RpcEncodable ProofWidgets.ExprPresentationData

Equations

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

structure ProofWidgets.ExprPresentations : Type

• presentations : Array ProofWidgets.ExprPresentationData

instance ProofWidgets.instRpcEncodableExprPresentations : Lean.Server.RpcEncodable ProofWidgets.ExprPresentations

Equations

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

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

Equations

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

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

Equations

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

structure ProofWidgets.GetExprPresentationParams : Type

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

  Name of the presenter to use.

instance ProofWidgets.instRpcEncodableGetExprPresentationParams : Lean.Server.RpcEncodable ProofWidgets.GetExprPresentationParams

Equations

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

@[deprecated]

def ProofWidgets.getExprPresentation : ProofWidgets.GetExprPresentationParams → Lean.Server.RequestM (Lean.Server.RequestTask ProofWidgets.Html)

Equations

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

structure ProofWidgets.ExprPresentationProps : Type

• expr : Lean.Server.WithRpcRef ProofWidgets.ExprWithCtx

instance ProofWidgets.instRpcEncodableExprPresentationProps : Lean.Server.RpcEncodable ProofWidgets.ExprPresentationProps

Equations

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

def ProofWidgets.ExprPresentation : ProofWidgets.Component ProofWidgets.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.