Documentation

Lean.Meta.Tactic.Grind.Internalize

source
def Lean.Meta.Grind.addCongrTable (e : Expr) :
GoalM Unit

Adds e to congruence table.

Instances For
    source
    def Lean.Meta.Grind.updateIndicesFound (k : HeadIndex) :
    GoalM Unit
    Instances For
      source
      def Lean.Meta.Grind.isMorallyIff (e : Expr) :
      Bool

      Returns true if e is of the form @Eq Prop a b

      Instances For
        source
        def Lean.Meta.Grind.preprocessTheorem (thm : EMatchTheorem) (generation : Nat) :
        GoalM EMatchTheorem
        Instances For
          source
          def Lean.Meta.Grind.activateTheorem (thm : EMatchTheorem) (generation : Nat) :
          GoalM Unit
          Instances For
            source
            def Lean.Meta.Grind.activateInjectiveTheorem (injThm : InjectiveTheorem) (generation : Nat) :
            GoalM Unit
            Instances For