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 ExprWithCtx
        Equations
          source
          def ProofWidgets.ExprWithCtx.runMetaM {α : Type} (e : ExprWithCtx) (x : Lean.Expr → Lean.MetaM α) :
          IO α
          Equations
            Instances For
              source
              def ProofWidgets.ExprWithCtx.save (e : Lean.Expr) :
              Lean.MetaM ExprWithCtx
              Equations
                Instances For