TorchLean API
Docs Home
Guide
Examples
Graphs
Aesop
.
BuiltinRules
.
Split
Search
Declaration colors
def
theorem
structure
axiom
return to top
source
Imports
Init
Lean.CoreM
Aesop.Frontend.Attribute
Aesop.Frontend.Extension
Aesop.Frontend.RuleExpr
Imported by
Aesop
.
BuiltinRules
.
splitTarget
Aesop
.
BuiltinRules
.
splitHypothesesCore
Aesop
.
BuiltinRules
.
splitHypotheses
source
def
Aesop
.
BuiltinRules
.
splitTarget
:
RuleTac
Instances For
source
partial def
Aesop
.
BuiltinRules
.
splitHypothesesCore
(
goal
:
Lean.MVarId
)
:
ScriptM
(
Option
(
Array
Lean.MVarId
)
)
source
def
Aesop
.
BuiltinRules
.
splitHypotheses
:
RuleTac
Instances For