Documentation

Lean.Meta.Tactic.Grind.MarkNestedSubsingletons

source
def Lean.Meta.Grind.isMarkedSubsingletonConst (e : Expr) :
Bool
Instances For
    source
    def Lean.Meta.Grind.isMarkedSubsingletonApp (e : Expr) :
    Bool
    Instances For
      source
      def Lean.Meta.Grind.markNestedSubsingletons (e : Expr) :
      GrindM Expr

      Wrap nested proofs and decidable instances in e with Lean.Grind.nestedProof and Lean.Grind.nestedDecidable-applications. Recall that the congruence closure module has special support for them.

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

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

        Instances For