Documentation

Lean.Meta.Tactic.Grind.MarkNestedProofs

source
unsafe def Lean.Meta.Grind.markNestedProofsImpl (e : Expr) :
MetaM Expr
Equations
    Instances For
      source
      unsafe def Lean.Meta.Grind.markNestedProofsImpl.visit (e : Expr) :
      StateRefT' IO.RealWorld (PtrMap Expr Expr) MetaM Expr
      Equations
        Instances For
          source
          def Lean.Meta.Grind.markNestedProofs (e : Expr) :
          MetaM Expr

          Wrap nested proofs e with Lean.Grind.nestedProof-applications. Recall that the congruence closure module has special support for Lean.Grind.nestedProof.

          Equations
            Instances For
              source
              def Lean.Meta.Grind.markProof (e : Expr) :
              MetaM Expr

              Given a proof e, mark it with Lean.Grind.nestedProof

              Equations
                Instances For