source
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

Instances For

source
opaque ProofWidgets.exprPresenters :
Lean.TagAttribute

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

source
@[implemented_by _private.ProofWidgets.Presentation.Expr.0.ProofWidgets.evalExprPresenterUnsafe]
opaque ProofWidgets.evalExprPresenter (env : Lean.Environment) (opts : Lean.Options) (constName : Lean.Name) :
Except String ExprPresenter
source
structure ProofWidgets.GetExprPresentationsParams :
Type

- expr : Lean.Server.WithRpcRef ExprWithCtx

Instances For

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

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

source
structure ProofWidgets.ExprPresentationData :
Type

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

Instances For

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

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

source
structure ProofWidgets.ExprPresentations :
Type

- presentations : Array ExprPresentationData

Instances For

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

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

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

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

Instances For

source
structure ProofWidgets.GetExprPresentationParams :
Type

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

  Name of the presenter to use.

Instances For

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

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

source
structure ProofWidgets.ExprPresentationProps :
Type

- expr : Lean.Server.WithRpcRef ExprWithCtx

Instances For

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

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

source
def ProofWidgets.ExprPresentation :
Component ExprPresentationProps

This component shows a selection of all known and applicable `ProofWidgets.ExprPresenter`s 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.

Instances For