Documentation

ProofWidgets.Compat

source
@[reducible, inline]
abbrev ProofWidgets.LazyEncodable (α : Type) :
Type

See RpcEncodable.

Instances For
    source
    structure ProofWidgets.ExprWithCtx :
    Type
    Instances For
      source
      @[implicit_reducible]
      instance ProofWidgets.instTypeNameExprWithCtx :
      TypeName ExprWithCtx
      source
      def ProofWidgets.ExprWithCtx.runMetaM {α : Type} (e : ExprWithCtx) (x : Lean.Expr → Lean.MetaM α) :
      IO α
      Instances For
        source
        def ProofWidgets.ExprWithCtx.save (e : Lean.Expr) :
        Lean.MetaM ExprWithCtx
        Instances For