Documentation
Aesop
.
Options
.
Internal
Search
return to top
source
Imports
Init
Aesop.Check
Aesop.Options.Public
Imported by
Aesop
.
Options'
Aesop
.
instInhabitedOptions'
Aesop
.
Options
.
toOptions'
source
structure
Aesop
.
Options'
extends
Aesop.Options
:
Type
strategy
:
Strategy
maxRuleApplicationDepth
:
Nat
maxRuleApplications
:
Nat
maxGoals
:
Nat
maxNormIterations
:
Nat
maxSafePrefixRuleApplications
:
Nat
maxRuleHeartbeats
:
Nat
maxSimpHeartbeats
:
Nat
maxUnfoldHeartbeats
:
Nat
applyHypsTransparency
:
Lean.Meta.TransparencyMode
assumptionTransparency
:
Lean.Meta.TransparencyMode
destructProductsTransparency
:
Lean.Meta.TransparencyMode
introsTransparency?
:
Option
Lean.Meta.TransparencyMode
terminal
:
Bool
warnOnNonterminal
:
Bool
traceScript
:
Bool
enableSimp
:
Bool
useSimpAll
:
Bool
useDefaultSimpSet
:
Bool
enableUnfold
:
Bool
generateScript :
Bool
forwardMaxDepth? :
Option
Nat
Instances For
source
instance
Aesop
.
instInhabitedOptions'
:
Inhabited
Options'
Equations
Aesop.instInhabitedOptions'
=
{
default
:=
{
toOptions
:=
default
,
generateScript
:=
default
,
forwardMaxDepth?
:=
default
}
}
source
def
Aesop
.
Options
.
toOptions'
{m :
Type
→
Type
}
[
Monad
m
]
[
Lean.MonadOptions
m
]
(opts :
Options
)
(forwardMaxDepth? :
Option
Nat
:=
none
)
:
m
Options'
Equations
One or more equations did not get rendered due to their size.
Instances For