Documentation

Aesop.BuiltinRules.Split

source
def Aesop.BuiltinRules.splitTarget :
RuleTac
Equations
    Instances For
      source
      partial def Aesop.BuiltinRules.splitHypothesesCore (goal : Lean.MVarId) :
      ScriptM (Option (Array Lean.MVarId))
      source
      def Aesop.BuiltinRules.splitHypotheses :
      RuleTac
      Equations
        Instances For