def Aesop.BuiltinRules.splitTarget : Aesop.RuleTac

Equations

• One or more equations did not get rendered due to their size.

def Aesop.BuiltinRules.splitFirstHypothesis (goal : Lean.MVarId) : Lean.MetaM (Option (Array Lean.MVarId))

Equations

• One or more equations did not get rendered due to their size.

def Aesop.BuiltinRules.splitHypothesesCore (goal : Lean.MVarId) : Lean.MetaM (Option (Array Lean.MVarId))

Equations

• Aesop.BuiltinRules.splitHypothesesCore goal = Lean.Meta.saturate1 goal Aesop.BuiltinRules.splitFirstHypothesis

def Aesop.BuiltinRules.tacticAesop_split_hyps : Lean.ParserDescr

Equations

• Aesop.BuiltinRules.tacticAesop_split_hyps = Lean.ParserDescr.node `Aesop.BuiltinRules.tacticAesop_split_hyps 1024 (Lean.ParserDescr.nonReservedSymbol "aesop_split_hyps" false)

def Aesop.BuiltinRules.splitHypotheses : Aesop.RuleTac

Equations

• One or more equations did not get rendered due to their size.