Options
Mathlib version: 2bb0410843932d03ff2c12cd9bf2e996f514a36b
Mathlib.Tactic.TFAE.useDeprecated
type: Bool
default: false
Re-enable "goal-style" 'tfae_have' syntax
aesop.check.all
type: Bool
default: false
(aesop) Enable all runtime checks. Individual checks can still be disabled.
aesop.check.proofReconstruction
type: Bool
default: false
(aesop) Typecheck partial proof terms during proof reconstruction.
aesop.check.rules
type: Bool
default: false
(aesop) Check that information reported by rules is correct.
aesop.check.script
type: Bool
default: false
(aesop) Check that the tactic script generated by Aesop proves the goal. When this check is active, Aesop generates a tactic script even if the user did not request one.
aesop.check.script.steps
type: Bool
default: false
(aesop) Check each step of the tactic script generated by Aesop. When this check is active, Aesop generates a tactic script even if the user did not request one.
aesop.check.tree
type: Bool
default: false
(aesop) Check search tree invariants after every iteration of the search loop. Quite expensive.
aesop.collectStats
type: Bool
default: false
(aesop) collect statistics about Aesop invocations. Use #aesop_stats to display the collected statistics.
aesop.dev.dynamicStructuring
type: Bool
default: true
(aesop) Only for use by Aesop developers. Enables dynamic script structuring.
aesop.dev.generateScript
type: Bool
default: false
(aesop) Only for use by Aesop developers. Generates a script even if none was requested.
aesop.dev.optimizedDynamicStructuring
type: Bool
default: true
(aesop) Only for use by Aesop developers. Uses static structuring instead of dynamic structuring if no metavariables appear in the proof.
aesop.smallErrorMessages
type: Bool
default: false
(aesop) Print smaller error messages. Used for testing.
aesop.warn.applyIff
type: Bool
default: true
(aesop) Warn when apply builder is applied to a rule with conclusion of the form A ↔ B
allowUnsafeReducibility
type: Bool
default: false
enables users to modify the reducibility settings for declarations even when such changes are deemed potentially hazardous. For example, simp and type class resolution maintain term indices where reducible declarations are expanded.
autoImplicit
type: Bool
default: true
Unbound local variables in declaration headers become implicit arguments. In "relaxed" mode (default), any atomic identifier is eligible, otherwise only single character followed by numeric digits are eligible. For example, def f (x : Vector α n) : Vector α n := automatically introduces the implicit variables {α n}.
autoLift
type: Bool
default: true
insert monadic lifts (i.e., liftM and coercions) when needed
backward.eqns.deepRecursiveSplit
type: Bool
default: true
Create equational lemmas for recursive functions like for non-recursive functions. If disabled, match statements in recursive function definitions that do not contain recursive calls do not cause further splits in the equational lemmas. This was the behavior before Lean 4.12, and the purpose of this option is to help migrating old code.
backward.eqns.nonrecursive
type: Bool
default: true
Create fine-grained equational lemmas even for non-recursive definitions.
backward.isDefEq.lazyProjDelta
type: Bool
default: true
use lazy delta reduction when solving unification constrains of the form (f a).i =?= (g b).i
backward.isDefEq.lazyWhnfCore
type: Bool
default: true
specifies transparency mode when normalizing constraints of the form (f a).i =?= s, if true only reducible definitions and instances are unfolded when reducing f a. Otherwise, the default setting is used
backward.synthInstance.canonInstances
type: Bool
default: true
use optimization that relies on 'morally canonical' instances during type class resolution
bootstrap.genMatcherCode
type: Bool
default: true
disable code generation for auxiliary matcher function
bootstrap.inductiveCheckResultingUniverse
type: Bool
default: true
by default the inductive/structure commands report an error if the resulting universe is not zero, but may be zero for some universe parameters. Reason: unless this type is a subsingleton, it is hardly what the user wants since it can only eliminate into Prop. In the Init package, we define subsingletons, and we use this option to disable the check. This option may be deleted in the future after we improve the validator
bv.ac_nf
type: Bool
default: false
Canonicalize with respect to associativity and commutativitiy.
checkBinderAnnotations
type: Bool
default: true
check whether type is a class instance whenever the binder annotation [...] is used
compiler.check
type: Bool
default: true
type check code after each compiler step (this is useful for debugging purses)
compiler.checkTypes
type: Bool
default: false
(compiler) perform type compatibility checking after each compiler pass. Note this is not a complete check, and it is used only for debugging purposes. It fails in code that makes heavy use of dependent types.
compiler.enableNew
type: Bool
default: false
(compiler) enable the new code generator, this should have no significant effect on your code but it does help to test the new code generator; unset to only use the old code generator instead
compiler.extract_closed
type: Bool
default: true
(compiler) enable/disable closed term caching
compiler.maxRecInline
type: Nat
default: 1
(compiler) maximum number of times a recursive definition tagged with [inline] can be recursively inlined before generating an error during compilation.
compiler.maxRecInlineIfReduce
type: Nat
default: 16
(compiler) maximum number of times a recursive definition tagged with [inline_if_reduce] can be recursively inlined before generating an error during compilation.
compiler.reuse
type: Bool
default: true
heuristically insert reset/reuse instruction pairs
compiler.small
type: Nat
default: 1
(compiler) function declarations with size ≤ small is inlined even if there are multiple occurrences.
debug.bv.graphviz
type: Bool
default: false
Output the AIG of bv_decide as graphviz into a file called aig.gv in the working directory of the Lean process.
debug.byAsSorry
type: Bool
default: false
replace by .. blocks with sorry IF the expected type is a proposition
debug.moduleNameAtTimeout
type: Bool
default: true
include module name in deterministic timeout error messages. Remark: we set this option to false to increase the stability of our test suite
debug.rawDecreasingByGoal
type: Bool
default: false
Shows the raw decreasing_by goal including internal implementation detail instead of cleaning it up with the clean_wf tactic. Can be enabled for debugging purposes. Please report an issue if you have to use this option for other reasons.
debug.skipKernelTC
type: Bool
default: false
skip kernel type checker. WARNING: setting this option to true may compromise soundness because your proofs will not be checked by the Lean kernel
deprecated.oldSectionVars
type: Bool
default: false
re-enable deprecated behavior of including exactly the section variables used in a declaration
diagnostics
type: Bool
default: false
collect diagnostic information
diagnostics.threshold
type: Nat
default: 20
only diagnostic counters above this threshold are reported by the definitional equality
diagnostics.threshold.proofSize
type: Nat
default: 16384
only display proof statistics when proof has at least this number of terms
eval.derive.repr
type: Bool
default: true
('#eval' command) enables auto-deriving 'Repr' instances as a fallback
eval.pp
type: Bool
default: true
('#eval' command) enables using 'ToExpr' instances to pretty print the result, otherwise uses 'Repr' or 'ToString' instances
eval.type
type: Bool
default: false
('#eval' command) enables pretty printing the type of the result
exponentiation.threshold
type: Nat
default: 256
maximum value for which exponentiation operations are safe to evaluate. When an exponent is a value greater than this threshold, the exponentiation will not be evaluated, and a warning will be logged. This helps to prevent the system from becoming unresponsive due to excessively large computations.
format.indent
type: Nat
default: 2
indentation
format.inputWidth
type: Nat
default: 100
ideal input width
format.unicode
type: Bool
default: true
unicode characters
format.width
type: Nat
default: 120
indentation
genInjectivity
type: Bool
default: true
generate injectivity theorems for inductive datatype constructors
genSizeOf
type: Bool
default: true
generate SizeOf instance for inductive types and structures
genSizeOfSpec
type: Bool
default: true
generate SizeOf specification theorems for automatically generated instances
guard_msgs.diff
type: Bool
default: false
When true, show a diff between expected and actual messages if they don't match.
hygiene
type: Bool
default: true
Annotate identifiers in quotations such that they are resolved relative to the scope at their declaration, not that at their eventual use/expansion, to avoid accidental capturing. Note that quotations/notations already defined are unaffected.
inductive.autoPromoteIndices
type: Bool
default: true
Promote indices to parameters in inductive types whenever possible.
infoview.maxTraceChildren
type: Nat
default: 50
Number of trace node children to display by default
internal.cmdlineSnapshots
type: Bool
default: false
mark persistent and reduce information stored in snapshots to the minimum necessary for the cmdline driver: diagnostics per command and final full snapshot
internal.parseQuotWithCurrentStage
type: Bool
default: false
(Lean bootstrapping) use parsers from the current stage inside quotations
interpreter.prefer_native
type: Bool
default: true
(interpreter) whether to use precompiled code where available
lang.lemmaCmd
type: Bool
default: false
enable the use of the lemma command as a synonym for theorem
leansearch.queries
type: Nat
default: 6
Number of results requested from leansearch (default 6)
leansearchclient.useragent
type: String
default: "LeanSearchClient"
Username for leansearchclient
linter.admit
type: Bool
default: false
enable the admit linter
linter.all
type: Bool
default: false
enable all linters
linter.constructorNameAsVariable
type: Bool
default: true
enable the linter that warns when bound variable names are nullary constructor names
linter.deprecated
type: Bool
default: true
if true, generate deprecation warnings
linter.docPrime
type: Bool
default: false
enable the docPrime linter
linter.dupNamespace
type: Bool
default: true
enable the duplicated namespace linter
linter.existingAttributeWarning
type: Bool
default: true
Linter, mostly used by @[to_additive], that checks that the source declaration doesn't have certain attributes
linter.flexible
type: Bool
default: false
enable the flexible linter
linter.globalAttributeIn
type: Bool
default: true
enable the globalAttributeIn linter
linter.hashCommand
type: Bool
default: false
enable the #-command linter
linter.haveLet
type: Nat
default: 0
enable the have vs let linter:
* 0 -- inactive;
* 1 -- active only on noisy declarations;
* 2 or more -- always active.
linter.minImports
type: Bool
default: false
enable the minImports linter
linter.minImports.increases
type: Bool
default: true
enable reporting increase-size change in the minImports linter
linter.missingDocs
type: Bool
default: false
enable the 'missing documentation' linter
linter.oldObtain
type: Bool
default: false
enable the oldObtain linter
linter.omit
type: Bool
default: false
enable the 'avoid omit' linter
linter.ppRoundtrip
type: Bool
default: false
enable the ppRoundtrip linter
linter.refine
type: Bool
default: false
enable the refine linter
linter.simpsNoConstructor
type: Bool
default: true
Linter to check that simps! is used
linter.simpsUnusedCustomDeclarations
type: Bool
default: true
Linter to check that no unused custom declarations are declared for simps
linter.style.cdot
type: Bool
default: false
enable the cdot linter
linter.style.dollarSyntax
type: Bool
default: false
enable the dollarSyntax linter
linter.style.header
type: Bool
default: false
enable the header style linter
linter.style.lambdaSyntax
type: Bool
default: false
enable the lambdaSyntax linter
linter.style.longFile
type: Nat
default: 0
enable the longFile linter
linter.style.longFileDefValue
type: Nat
default: 1500
a soft upper bound on the number of lines of each file
linter.style.longLine
type: Bool
default: false
enable the longLine linter
linter.style.missingEnd
type: Bool
default: false
enable the missing end linter
linter.style.multiGoal
type: Bool
default: false
enable the multiGoal linter
linter.style.setOption
type: Bool
default: false
enable the setOption linter
linter.suspiciousUnexpanderPatterns
type: Bool
default: true
enable the 'suspicious unexpander patterns' linter
linter.toAdditiveExisting
type: Bool
default: true
Linter used by @[to_additive] that checks whether the user correctly specified that
the additive declaration already exists
linter.toAdditiveGenerateName
type: Bool
default: true
Linter used by @[to_additive] that checks if @[to_additive] automatically generates the user-given name
linter.toAdditiveReorder
type: Bool
default: true
Linter to check that the reorder attribute is not given manually.
linter.unnecessarySeqFocus
type: Bool
default: true
enable the 'unnecessary <;>' linter
linter.unnecessarySimpa
type: Bool
default: true
enable the 'unnecessary simpa' linter
linter.unreachableTactic
type: Bool
default: true
enable the 'unreachable tactic' linter
linter.unusedRCasesPattern
type: Bool
default: true
enable the 'unused rcases pattern' linter
linter.unusedSectionVars
type: Bool
default: true
enable the 'unused section variables in theorem body' linter
linter.unusedTactic
type: Bool
default: true
enable the unused tactic linter
linter.unusedVariables
type: Bool
default: true
enable the 'unused variables' linter
linter.unusedVariables.analyzeTactics
type: Bool
default: false
enable analysis of local variables in presence of tactic proofs
By default, the linter will limit itself to linting a declaration's parameters whenever tactic proofs are present as these can be expensive to analyze. Enabling this option extends linting to local variables both inside and outside tactic proofs, though it can also lead to some false negatives as intermediate tactic states may reference some variables without the declaration ultimately depending on them.
linter.unusedVariables.funArgs
type: Bool
default: true
enable the 'unused variables' linter to mark unused function arguments
linter.unusedVariables.patternVars
type: Bool
default: true
enable the 'unused variables' linter to mark unused pattern variables
linter.upstreamableDecl
type: Bool
default: false
enable the upstreamableDecl linter
loogle.queries
type: Nat
default: 6
Number of results requested from loogle (default 6)
match.ignoreUnusedAlts
type: Bool
default: false
if true, do not generate error if an alternative is not used
maxBackwardChainingDepth
type: Nat
default: 10
The maximum search depth used in the backwards chaining part of the proof of brecOn for inductive predicates.
maxHeartbeats
type: Nat
default: 200000
maximum amount of heartbeats per command. A heartbeat is number of (small) memory allocations (in thousands), 0 means no limit
maxRecDepth
type: Nat
default: 512
maximum recursion depth for many Lean procedures
maxSynthPendingDepth
type: Nat
default: 1
maximum number of nested synthPending invocations. When resolving unification constraints, pending type class problems may need to be synthesized. These type class problems may create new unification constraints that again require solving new type class problems. This option puts a threshold on how many nested problems are created.
maxUniverseOffset
type: Nat
default: 32
maximum universe level offset
moogle.queries
type: Nat
default: 6
Number of results requested from moogle (default 6)
pp.all
type: Bool
default: false
(pretty printer) display coercions, implicit parameters, proof terms, fully qualified names, universe, and disable beta reduction and notations during pretty printing
pp.analyze
type: Bool
default: false
(pretty printer analyzer) determine annotations sufficient to ensure round-tripping
pp.analyze.checkInstances
type: Bool
default: false
(pretty printer analyzer) confirm that instances can be re-synthesized
pp.analyze.explicitHoles
type: Bool
default: false
(pretty printer analyzer) use _ for explicit arguments that can be inferred
pp.analyze.knowsType
type: Bool
default: true
(pretty printer analyzer) assume the type of the original expression is known
pp.analyze.omitMax
type: Bool
default: true
(pretty printer analyzer) omit universe max annotations (these constraints can actually hurt)
pp.analyze.trustId
type: Bool
default: true
(pretty printer analyzer) always assume an implicit fun x => x can be inferred
pp.analyze.trustKnownFOType2TypeHOFuns
type: Bool
default: true
(pretty printer analyzer) omit higher-order functions whose values seem to be knownType2Type
pp.analyze.trustOfNat
type: Bool
default: true
(pretty printer analyzer) always 'pretend' OfNat.ofNat applications can elab bottom-up
pp.analyze.trustOfScientific
type: Bool
default: true
(pretty printer analyzer) always 'pretend' OfScientific.ofScientific applications can elab bottom-up
pp.analyze.trustSubst
type: Bool
default: false
(pretty printer analyzer) always 'pretend' applications that can delab to â–¸ are 'regular'
pp.analyze.trustSubtypeMk
type: Bool
default: true
(pretty printer analyzer) assume the implicit arguments of Subtype.mk can be inferred
pp.analyze.typeAscriptions
type: Bool
default: true
(pretty printer analyzer) add type ascriptions when deemed necessary
pp.auxDecls
type: Bool
default: false
display auxiliary declarations used to compile recursive functions
pp.beta
type: Bool
default: false
(pretty printer) apply beta-reduction when pretty printing
pp.coercions
type: Bool
default: true
(pretty printer) hide coercion applications
pp.deepTerms
type: Bool
default: false
(pretty printer) display deeply nested terms, replacing them with ⋯ if set to false
pp.deepTerms.threshold
type: Nat
default: 50
(pretty printer) when pp.deepTerms is false, the depth at which terms start being replaced with ⋯
pp.explicit
type: Bool
default: false
(pretty printer) display implicit arguments
pp.exprSizes
type: Bool
default: false
(pretty printer) prefix each embedded expression with its sizes in the format (size disregarding sharing/size with sharing/size with max sharing)
pp.fieldNotation
type: Bool
default: true
(pretty printer) use field notation when pretty printing, including for structure projections, unless '@[pp_nodot]' is applied
pp.fieldNotation.generalized
type: Bool
default: true
(pretty printer) when pp.fieldNotation is true, enable using generalized field notation when the argument for field notation is the first explicit argument
pp.fullNames
type: Bool
default: false
(pretty printer) display fully qualified names
pp.funBinderTypes
type: Bool
default: false
(pretty printer) display types of lambda parameters
pp.implementationDetailHyps
type: Bool
default: false
display implementation detail hypotheses in the local context
pp.inaccessibleNames
type: Bool
default: true
display inaccessible declarations in the local context
pp.instanceTypes
type: Bool
default: false
(pretty printer) when printing explicit applications, show the types of inst-implicit arguments
pp.instances
type: Bool
default: true
(pretty printer) if set to false, replace inst-implicit arguments to explicit applications with placeholders
pp.instantiateMVars
type: Bool
default: true
(pretty printer) instantiate mvars before delaborating
pp.letVarTypes
type: Bool
default: false
(pretty printer) display types of let-bound variables
pp.macroStack
type: Bool
default: false
display macro expansion stack
pp.match
type: Bool
default: true
(pretty printer) disable/enable 'match' notation
pp.maxSteps
type: Nat
default: 5000
(pretty printer) maximum number of expressions to visit, after which terms will pretty print as ⋯
pp.motives.all
type: Bool
default: false
(pretty printer) print all motives
pp.motives.nonConst
type: Bool
default: false
(pretty printer) print all motives that are not constant functions
pp.motives.pi
type: Bool
default: true
(pretty printer) print all motives that return pi types
pp.mvars
type: Bool
default: true
(pretty printer) display names of metavariables when true, and otherwise display them as '?' (for expression metavariables) and as '' (for universe level metavariables)
pp.mvars.anonymous
type: Bool
default: true
(pretty printer) display names for auto-generated metavariables such as ?m.22 when true, and otherwise display them as '?' (for expression metavariables) and as '' (for universe level metavariables). When 'pp.mvars' is false, this is 'false' as well.
pp.mvars.delayed
type: Bool
default: false
(pretty printer) display delayed assigned metavariables when true, otherwise display what they are assigned to
pp.mvars.levels
type: Bool
default: true
(pretty printer) display universe level metavariables as ?u.22 when true, and otherwise display them as '_'. When either 'pp.mvars' or 'pp.mvars.anonymous' is false, this is 'false' as well.
pp.mvars.withType
type: Bool
default: false
(pretty printer) display metavariables with a type ascription
pp.natLit
type: Bool
default: false
(pretty printer) display raw natural number literals with nat_lit prefix
pp.notation
type: Bool
default: true
(pretty printer) disable/enable notation (infix, mixfix, postfix operators and unicode characters)
pp.numericTypes
type: Bool
default: false
(pretty printer) display types of numeric literals
pp.oneline
type: Bool
default: false
(pretty printer) elide all but first line of pretty printer output
pp.piBinderTypes
type: Bool
default: true
(pretty printer) display types of pi parameters
pp.privateNames
type: Bool
default: false
(pretty printer) display internal names assigned to private declarations
pp.proofs
type: Bool
default: false
(pretty printer) display proofs when true, and replace proofs appearing within expressions by ⋯ when false
pp.proofs.threshold
type: Nat
default: 0
(pretty printer) when pp.proofs is false, controls the complexity of proofs at which they begin being replaced with ⋯
pp.proofs.withType
type: Bool
default: false
(pretty printer) when pp.proofs is false, adds a type ascription to the omitted proof
pp.qq
type: Bool
default: true
(pretty printer) print quotations as q(...) and Q(...)
pp.raw
type: Bool
default: false
(pretty printer) print raw expression/syntax tree
pp.raw.maxDepth
type: Nat
default: 32
(pretty printer) maximum Syntax depth for raw printer
pp.raw.showInfo
type: Bool
default: false
(pretty printer) print SourceInfo metadata with raw printer
pp.rawOnError
type: Bool
default: false
(pretty printer) fallback to 'raw' printer when pretty printer fails
pp.safeShadowing
type: Bool
default: true
(pretty printer) allow variable shadowing if there is no collision
pp.sanitizeNames
type: Bool
default: true
add suffix to shadowed/inaccessible variables when pretty printing
pp.showLetValues
type: Bool
default: true
display let-declaration values in the info view
pp.structureInstanceTypes
type: Bool
default: false
(pretty printer) display type of structure instances
pp.structureInstances
type: Bool
default: true
(pretty printer) display structure instances using the '{ fieldName := fieldValue, ... }' notation, or using '⟨fieldValue, ... ⟩' if structure is tagged with the '@[pp_using_anonymous_constructor]' attribute
pp.structureInstances.flatten
type: Bool
default: true
(pretty printer) flatten nested structure instances for parent projections
pp.tagAppFns
type: Bool
default: false
(pretty printer) tag all constants that are the function in a function application
pp.unicode.fun
type: Bool
default: false
(pretty printer) disable/enable unicode ↦ notation for functions
pp.universes
type: Bool
default: false
(pretty printer) display universe
printMessageEndPos
type: Bool
default: false
print end position of each message in addition to start position
profiler
type: Bool
default: false
show exclusive execution times of various Lean components
See also trace.profiler for an alternative profiling system with structured output.
profiler.threshold
type: Nat
default: 100
threshold in milliseconds, profiling times under threshold will not be reported individually
push_neg.use_distrib
type: Bool
default: false
Make push_neg use not_and_or rather than the default not_and.
quotPrecheck
type: Bool
default: true
Enable eager name analysis on notations in order to find unbound identifiers early. Note that type-sensitive syntax ("elaborators") needs special support for this kind of check, so it might need to be turned off when using such syntax.
quotPrecheck.allowSectionVars
type: Bool
default: false
Allow occurrences of section variables in checked quotations, it is useful when declaring local notation.
relaxedAutoImplicit
type: Bool
default: true
When "relaxed" mode is enabled, any atomic nonempty identifier is eligible for auto bound implicit locals (see option autoImplicit).
sat.binaryProofs
type: Bool
default: true
Whether to use the binary LRAT proof format. Currently set to false and ignored on Windows due to a bug in CaDiCal.
sat.solver
type: String
default: ""
Name of the SAT solver used by Lean.Elab.Tactic.BVDecide tactics.
1. If this is set to something besides the empty string they will use that binary.
2. If this is set to the empty string they will check if there is a cadical binary next to theexecuting program. Usually that program is going to be `lean` itself and we do ship a`cadical` next to it.
3. If that does not succeed try to call `cadical` from PATH. The empty string default indicatesto use the one that ships with Lean.
sat.timeout
type: Nat
default: 10
the number of seconds that the sat solver is run before aborting
sat.trimProofs
type: Bool
default: true
Whether to run the trimming algorithm on LRAT proofs
says.no_verify_in_CI
type: Bool
default: false
Disable reverification, even if the CI environment variable is set.
says.verify
type: Bool
default: false
For every appearance of the X says Y combinator, re-verify that running X produces Try this: Y.
server.reportDelayMs
type: Nat
default: 200
(server) time in milliseconds to wait before reporting progress and diagnostics on document edit in order to reduce flickering
This option can only be set on the command line, not in the lakefile or via set_option.
showInferredTerminationBy
type: Bool
default: false
In recursive definitions, show the inferred termination_by measure.
showPartialSyntaxErrors
type: Bool
default: false
show elaboration errors from partial syntax trees (i.e. after parser recovery)
showTacticDiff
type: Bool
default: true
When true, interactive goals for tactics will be decorated with diffing information.
simprocs
type: Bool
default: true
Enable/disable simprocs (simplification procedures).
smartUnfolding
type: Bool
default: true
when computing weak head normal form, use auxiliary definition created for functions defined by structural recursion
stderrAsMessages
type: Bool
default: true
(server) capture output to the Lean stderr channel (such as from dbg_trace) during elaboration of a command as a diagnostic message
structure.strictResolutionOrder
type: Bool
default: false
if true, require a strict resolution order for structures
structureDiamondWarning
type: Bool
default: false
if true, enable warnings when a structure has diamond inheritance
synthInstance.checkSynthOrder
type: Bool
default: true
check that instances do not introduce metavariable in non-out-params
synthInstance.maxHeartbeats
type: Nat
default: 20000
maximum amount of heartbeats per typeclass resolution problem. A heartbeat is number of (small) memory allocations (in thousands), 0 means no limit
synthInstance.maxSize
type: Nat
default: 128
maximum number of instances used to construct a solution in the type class instance synthesis procedure
tactic.customEliminators
type: Bool
default: true
enable using custom eliminators in the 'induction' and 'cases' tactics defined using the '@[induction_eliminator]' and '@[cases_eliminator]' attributes
tactic.dbg_cache
type: Bool
default: false
enable tactic cache debug messages (remark: they are sent to the standard error)
tactic.hygienic
type: Bool
default: true
make sure tactics are hygienic
tactic.simp.trace
type: Bool
default: false
When tracing is enabled, calls to simp or dsimp will print an equivalent simp only call.
tactic.skipAssignedInstances
type: Bool
default: true
in the rw and simp tactics, if an instance implicit argument is assigned, do not try to synthesize instance.
trace.Aesop.Util.EqualUpToIds
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.CancelDenoms
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Compiler
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Compiler.commonJoinPointArgs
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Compiler.cse
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Compiler.eagerLambdaLifting
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Compiler.elimDeadBranches
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Compiler.extendJoinPointContext
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Compiler.findJoinPoints
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Compiler.floatLetIn
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Compiler.init
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Compiler.jp
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Compiler.lambdaLifting
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Compiler.pullFunDecls
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Compiler.pullInstances
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Compiler.reduceArity
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Compiler.reduceJpArity
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Compiler.result
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Compiler.saveBase
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Compiler.saveMono
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Compiler.simp
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Compiler.simp.inline
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Compiler.simp.jpCases
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Compiler.simp.stat
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Compiler.simp.step
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Compiler.simp.step.new
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Compiler.specialize
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Compiler.specialize.candidate
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Compiler.specialize.info
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Compiler.specialize.step
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Compiler.stat
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Compiler.test
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Compiler.toMono
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Compiler.trace
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Debug.Meta.Tactic.cc
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Debug.Meta.Tactic.cc.ac
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Debug.Meta.Tactic.cc.parentOccs
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Debug.Meta.Tactic.fun_prop
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Debug.Meta.Tactic.simp
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Debug.Meta.Tactic.simp.congr
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.Deriving
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.Deriving.RpcEncodable
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.Deriving.beq
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.Deriving.decEq
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.Deriving.fintype
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.Deriving.fromJson
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.Deriving.hashable
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.Deriving.inhabited
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.Deriving.ord
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.Deriving.repr
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.Deriving.toExpr
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.Deriving.toJson
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.ProxyType
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.app
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.app.args
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.app.elab_as_elim
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.app.finalize
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.app.propagateExpectedType
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.autoParam
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.axiom
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.binop
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.binrel
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.cases
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.coe
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.command
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.congr
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.debug
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.defaultInstance
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.definition
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.definition.body
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.definition.eqns
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.definition.mkClosure
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.definition.scc
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.definition.structural
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.definition.structural.eqns
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.definition.unfoldEqn
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.definition.wf
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.definition.wf.eqns
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.do
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.eval
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.fbinop
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.implicitForall
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.induction
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.inductive
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.info
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.input
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.instance.mkInstanceName
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.let
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.let.decl
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.letrec
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.lint
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.match
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.match_syntax
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.match_syntax.alt
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.match_syntax.onMatch
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.match_syntax.result
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.postpone
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.resume
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.reuse
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.snapshotTree
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.step
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.step.result
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.struct
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.struct.modifyOp
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.structure
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.structure.resolutionOrder
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.tactic
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Elab.tactic.backtrack
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Kernel
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.AC
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.CongrTheorems
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.FunInd
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.IndPredBelow
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.IndPredBelow.match
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.IndPredBelow.search
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.Match
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.Match.debug
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.Match.match
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.Match.matchEqs
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.Match.unify
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.Tactic
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.Tactic.acyclic
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.Tactic.bv
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.Tactic.cases
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.Tactic.cc.failure
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.Tactic.cc.merge
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.Tactic.contradiction
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.Tactic.fun_prop
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.Tactic.fun_prop.attr
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.Tactic.induction
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.Tactic.polyrith
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.Tactic.sat
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.Tactic.simp
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.Tactic.simp.all
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.Tactic.simp.congr
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.Tactic.simp.discharge
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.Tactic.simp.ground
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.Tactic.simp.heads
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.Tactic.simp.numSteps
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.Tactic.simp.rewrite
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.Tactic.simp.unify
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.Tactic.solveByElim
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.Tactic.splitIf
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.Tactic.subst
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.appBuilder
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.appBuilder.error
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.appBuilder.result
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.check
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.debug
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.gcongr
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.injective
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.isDefEq
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.isDefEq.assign
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.isDefEq.assign.beforeMkLambda
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.isDefEq.assign.checkTypes
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.isDefEq.assign.occursCheck
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.isDefEq.assign.outOfScopeFVar
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.isDefEq.assign.readOnlyMVarWithBiggerLCtx
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.isDefEq.assign.typeError
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.isDefEq.cache
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.isDefEq.constApprox
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.isDefEq.delta
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.isDefEq.delta.unfoldLeft
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.isDefEq.delta.unfoldLeftRight
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.isDefEq.delta.unfoldRight
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.isDefEq.eta.struct
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.isDefEq.foApprox
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.isDefEq.hint
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.isDefEq.onFailure
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.isDefEq.stuck
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.isDefEq.stuckMVar
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.isDefEq.whnf.reduceBinOp
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.isLevelDefEq
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.isLevelDefEq.postponed
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.isLevelDefEq.step
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.isLevelDefEq.stuck
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.sizeOf
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.sizeOf.aux
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.sizeOf.loop
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.sizeOf.minor
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.sizeOf.minor.step
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.synthInstance
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.synthInstance.answer
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.synthInstance.instances
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.synthInstance.newAnswer
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.synthInstance.resume
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.synthInstance.tryResolve
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.synthInstance.unusedArgs
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.synthOrder
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.synthPending
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Meta.whnf
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.PrettyPrinter
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.PrettyPrinter.delab
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.PrettyPrinter.delab.input
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.PrettyPrinter.format
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.PrettyPrinter.format.backtrack
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.PrettyPrinter.format.input
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.PrettyPrinter.parenthesize
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.PrettyPrinter.parenthesize.backtrack
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.PrettyPrinter.parenthesize.input
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Tactic.compute_degree
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Tactic.congrm
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Tactic.field_simp
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Tactic.generalize_proofs
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Tactic.librarySearch
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Tactic.librarySearch.lemmas
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Tactic.move_oper
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Tactic.norm_cast
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Tactic.norm_num
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Tactic.positivity
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Tactic.positivity.failure
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Tactic.propose
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Tactic.rewrites
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Tactic.rewrites.lemmas
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.Tactic.trans
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.abel
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.abel.detail
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.adaptationNote
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.aesop
type: Bool
default: false
(aesop) Print actions taken by Aesop during the proof search.
trace.aesop.debug
type: Bool
default: false
(aesop) Print various debugging information.
trace.aesop.extraction
type: Bool
default: false
(aesop) Print a trace of the proof extraction procedure.
trace.aesop.proof
type: Bool
default: false
(aesop) If the search is successful, print the produced proof term.
trace.aesop.ruleSet
type: Bool
default: false
(aesop) Print the rule set before starting the search.
trace.aesop.script
type: Bool
default: false
(aesop) Print a trace of script generation.
trace.aesop.stats
type: Bool
default: false
(aesop) If the search is successful, print some statistics.
trace.aesop.tree
type: Bool
default: false
(aesop) Once the search has concluded (successfully or unsuccessfully), print the final search tree.
trace.apply_fun
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.bicategory
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.bound.attribute
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.compiler
type: Bool
default: false
(trace) enable/disable tracing for the given module and submodules
trace.compiler.cce
type: Bool
default: false
(trace) enable/disable tracing for the given module and submodules
trace.compiler.code_gen
type: Bool
default: false
(trace) enable/disable tracing for the given module and submodules
trace.compiler.cse
type: Bool
default: false
(trace) enable/disable tracing for the given module and submodules
trace.compiler.eager_lambda_lifting
type: Bool
default: false
(trace) enable/disable tracing for the given module and submodules
trace.compiler.elim_dead_let
type: Bool
default: false
(trace) enable/disable tracing for the given module and submodules
trace.compiler.erase_irrelevant
type: Bool
default: false
(trace) enable/disable tracing for the given module and submodules
trace.compiler.eta_expand
type: Bool
default: false
(trace) enable/disable tracing for the given module and submodules
trace.compiler.extract_closed
type: Bool
default: false
(trace) enable/disable tracing for the given module and submodules
trace.compiler.inline
type: Bool
default: false
(trace) enable/disable tracing for the given module and submodules
trace.compiler.input
type: Bool
default: false
(trace) enable/disable tracing for the given module and submodules
trace.compiler.ir
type: Bool
default: false
(trace) enable/disable tracing for the given module and submodules
trace.compiler.ir.borrow
type: Bool
default: false
(trace) enable/disable tracing for the given module and submodules
trace.compiler.ir.boxing
type: Bool
default: false
(trace) enable/disable tracing for the given module and submodules
trace.compiler.ir.elim_dead
type: Bool
default: false
(trace) enable/disable tracing for the given module and submodules
trace.compiler.ir.elim_dead_branches
type: Bool
default: false
(trace) enable/disable tracing for the given module and submodules
trace.compiler.ir.expand_reset_reuse
type: Bool
default: false
(trace) enable/disable tracing for the given module and submodules
trace.compiler.ir.init
type: Bool
default: false
(trace) enable/disable tracing for the given module and submodules
trace.compiler.ir.push_proj
type: Bool
default: false
(trace) enable/disable tracing for the given module and submodules
trace.compiler.ir.rc
type: Bool
default: false
(trace) enable/disable tracing for the given module and submodules
trace.compiler.ir.reset_reuse
type: Bool
default: false
(trace) enable/disable tracing for the given module and submodules
trace.compiler.ir.result
type: Bool
default: false
(trace) enable/disable tracing for the given module and submodules
trace.compiler.ir.simp_case
type: Bool
default: false
(trace) enable/disable tracing for the given module and submodules
trace.compiler.lambda_lifting
type: Bool
default: false
(trace) enable/disable tracing for the given module and submodules
trace.compiler.lambda_pure
type: Bool
default: false
(trace) enable/disable tracing for the given module and submodules
trace.compiler.lcnf
type: Bool
default: false
(trace) enable/disable tracing for the given module and submodules
trace.compiler.ll_infer_type
type: Bool
default: false
(trace) enable/disable tracing for the given module and submodules
trace.compiler.llnf
type: Bool
default: false
(trace) enable/disable tracing for the given module and submodules
trace.compiler.optimize_bytecode
type: Bool
default: false
(trace) enable/disable tracing for the given module and submodules
trace.compiler.reduce_arity
type: Bool
default: false
(trace) enable/disable tracing for the given module and submodules
trace.compiler.result
type: Bool
default: false
(trace) enable/disable tracing for the given module and submodules
trace.compiler.simp
type: Bool
default: false
(trace) enable/disable tracing for the given module and submodules
trace.compiler.simp_app_args
type: Bool
default: false
(trace) enable/disable tracing for the given module and submodules
trace.compiler.simp_detail
type: Bool
default: false
(trace) enable/disable tracing for the given module and submodules
trace.compiler.simp_float_cases
type: Bool
default: false
(trace) enable/disable tracing for the given module and submodules
trace.compiler.spec_candidate
type: Bool
default: false
(trace) enable/disable tracing for the given module and submodules
trace.compiler.spec_info
type: Bool
default: false
(trace) enable/disable tracing for the given module and submodules
trace.compiler.specialize
type: Bool
default: false
(trace) enable/disable tracing for the given module and submodules
trace.compiler.stage1
type: Bool
default: false
(trace) enable/disable tracing for the given module and submodules
trace.compiler.stage2
type: Bool
default: false
(trace) enable/disable tracing for the given module and submodules
trace.compiler.struct_cases_on
type: Bool
default: false
(trace) enable/disable tracing for the given module and submodules
trace.congr!
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.congr!.synthesize
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.debug
type: Bool
default: false
(trace) enable/disable tracing for the given module and submodules
trace.explode
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.linarith
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.linarith.detail
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.monoidal
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.notation3
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.omega
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.pp.analyze
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.pp.analyze.annotate
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.pp.analyze.error
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.pp.analyze.tryUnify
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.profiler
type: Bool
default: false
activate nested traces with execution time above trace.profiler.threshold and annotate with time
trace.profiler.output
type: String
default: ""
output trace.profiler data in Firefox Profiler-compatible format to given file path
trace.profiler.output.pp
type: Bool
default: false
if false, limit text in exported trace nodes to trace class name and TraceData.tag, if any
This is useful when we are interested in the time taken by specific subsystems instead of specific invocations, which is the common case.
trace.profiler.threshold
type: Nat
default: 10
threshold in milliseconds (or heartbeats if trace.profiler.useHeartbeats is true), traces below threshold will not be activated
trace.profiler.useHeartbeats
type: Bool
default: false
if true, measure and report heartbeats instead of seconds
trace.rw_search
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.rw_search.detail
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.saturate
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.simps.debug
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.simps.verbose
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.split.debug
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.split.failure
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.string_diagram
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.tactic.use
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.tauto
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.to_additive
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.to_additive_detail
type: Bool
default: false
enable/disable tracing for the given module and submodules
trace.variable?
type: Bool
default: false
enable/disable tracing for the given module and submodules
variable?.checkRedundant
type: Bool
default: true
Warn if instance arguments can be inferred from preceding ones
variable?.maxSteps
type: Nat
default: 15
The maximum number of instance arguments variable? will try to insert before giving up
warningAsError
type: Bool
default: false
treat warnings as errors