Documentation
Aesop
.
BuiltinRules
.
Assumption
Search
return to top
source
Imports
Init
Aesop.Frontend.Attribute
Imported by
Aesop
.
BuiltinRules
.
assumption
Aesop
.
BuiltinRules
.
assumption
.
tryHyp
source
def
Aesop
.
BuiltinRules
.
assumption
:
RuleTac
Equations
Instances For
source
def
Aesop
.
BuiltinRules
.
assumption
.
tryHyp
(
goal
:
Lean.MVarId
)
(
fvarId
:
Lean.FVarId
)
(
md
:
Lean.Meta.TransparencyMode
)
:
BaseM
(
Option
(
RuleApplication
×
Bool
))
Equations
Instances For