Documentation

ProofWidgets.Compat

source
@[reducible, inline]
abbrev ProofWidgets.LazyEncodable (α : Type) :
Type
Equations
Instances For
    source
    structure ProofWidgets.ExprWithCtx :
    Type
    Instances For
      source
      instance ProofWidgets.instTypeNameExprWithCtx :
      TypeName ProofWidgets.ExprWithCtx
      Equations
      source
      def ProofWidgets.ExprWithCtx.runMetaM {α : Type} (e : ProofWidgets.ExprWithCtx) (x : Lean.Expr → Lean.MetaM α) :
      IO α
      Equations
      • e.runMetaM x = e.ci.runMetaM e.lctx (x e.expr)
      Instances For
        source
        def ProofWidgets.ExprWithCtx.save (e : Lean.Expr) :
        Lean.MetaM ProofWidgets.ExprWithCtx
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For