选项¶

Mathlib 版本: e4cf8333e0be712392567e370eead57e05d636a7

Elab.async¶

type: Bool default: false 收集诊断信息

diagnostics.threshold¶

type: Nat default: 20 仅报告定义等价性中超过此阈值的诊断计数器

diagnostics.threshold.proofSize¶

type: Nat default: 16384 仅当证明至少包含此数量项时显示证明统计信息

eval.derive.repr¶

type: Bool default: true ('#eval' 命令) 启用自动派生 'Repr' 实例作为回退

eval.pp¶

type: Bool default: true ('#eval' 命令) 启用使用 'ToExpr' 实例美化输出结果，否则使用 'Repr' 或 'ToString' 实例

eval.type¶

type: Bool default: false ('#eval' 命令) 启用美化输出结果的类型信息

exponentiation.threshold¶

type: Nat default: 256 幂运算安全评估的最大阈值。当指数值超过此阈值时，将不评估幂运算并记录警告。防止系统因过大计算量失去响应。

format.indent¶

type: Nat default: 2 缩进量

format.inputWidth¶

type: Nat default: 100 理想输入宽度

format.unicode¶

type: Bool default: true 使用Unicode字符

format.width¶

type: Nat default: 120 缩进宽度

genInjectivity¶

type: Bool default: true 为归纳数据类型构造器生成单射性定理

genSizeOf¶

type: Bool default: true 为归纳类型及结构体自动生成 SizeOf 实例

genSizeOfSpec¶

type: Bool default: true 为自动生成的实例生成 SizeOf 规范定理

grind.debug¶

type: Bool default: false 更新后检查不变量

grind.debug.proofs¶

type: Bool default: false 检查所有等价类元素间的证明

grind.warning¶

type: Bool default: true 禁用 grind 使用警告

guard_msgs.diff¶

type: Bool default: false 若为真，当预期与实际消息不匹配时显示差异对比

hygiene¶

type: Bool default: true 对引用中的标识符进行注解，使其解析基于声明时的作用域而非使用/扩展时的作用域，避免意外捕获。注意已有引用/表示法不受影响。

inductive.autoPromoteIndices¶

type: Bool default: true 在可能时将归纳类型的索引提升为参数

internal.cmdlineSnapshots¶

type: Bool default: false 将快照中存储的信息缩减至命令行驱动所需最小量：每条命令的诊断信息及最终完整快照

internal.parseQuotWithCurrentStage¶

type: Bool default: false (Lean 引导) 在引用中使用当前阶段的解析器

interpreter.prefer_native¶

type: Bool default: true (解释器) 在可用时优先使用预编译代码

lang.lemmaCmd¶

type: Bool default: false 启用 lemma 命令作为 theorem 的同义词

leansearch.queries¶

type: Nat default: 6 leansearch 请求的结果数量（默认 6）

leansearchclient.backend¶

type: String default: "leansearch" 默认使用的后端，可选值为 leansearch 或 moogle

leansearchclient.useragent¶

type: String default: "LeanSearchClient" leansearchclient 的用户代理名称

linter.admit¶

type: Bool default: false 启用 admit 检查器

linter.all¶

type: Bool default: false 启用所有检查器

linter.constructorNameAsVariable¶

type: Bool default: true 启用警告绑定变量名为零元构造器名称的检查器

linter.countHeartbeats¶

type: Bool default: false 启用心跳计数检查器

linter.countHeartbeatsApprox¶

type: Bool default: false 若为真，countHeartbeats 检查器将心跳计数向下取整至最接近的千位数

linter.deprecated¶

type: Bool default: true 若为真，生成弃用警告

linter.docPrime¶

type: Bool default: false 启用 docPrime 检查器

linter.dupNamespace¶

type: Bool default: true 启用重复命名空间检查器

linter.existingAttributeWarning¶

type: Bool default: true 检查源声明是否具有某些属性的检查器，主要由 @[to_additive] 使用

linter.flexible¶

type: Bool default: false 启用 flexible 检查器

linter.globalAttributeIn¶

type: Bool default: true 启用 globalAttributeIn 检查器

linter.hashCommand¶

type: Bool default: false 启用 # 命令检查器

linter.haveLet¶

type: Nat default: 0 启用 have 与 let 的检查： * 0 -- 不启用； * 1 -- 仅在存在噪音的声明中启用； * 2 或更高 -- 始终启用。

linter.indexVariables¶

type: Bool default: false 验证作为索引出现的变量（如 xs[i] 或 xs.take i 中的 i）仅为 i、j 或 k

linter.listVariables¶

type: Bool default: false 验证所有 List/Array/Vector 变量使用允许的名称

linter.minImports¶

type: Bool default: false 启用 minImports 检查器

linter.minImports.increases¶

type: Bool default: true 在 minImports 检查器中启用报告规模增长变化

linter.missingDocs¶

type: Bool default: false 启用“缺失文档”检查器

linter.oldObtain¶

type: Bool default: false 启用 oldObtain 检查器

linter.omit¶

type: Bool default: false 启用“避免 omit”检查器

linter.ppRoundtrip¶

type: Bool default: false 启用 ppRoundtrip 检查器

linter.simpsNoConstructor¶

type: Bool default: true 检查是否使用了 simps! 的检查器

linter.simpsUnusedCustomDeclarations¶

type: Bool default: true 检查是否为 simps 声明了未使用的自定义声明的检查器

linter.style.cases¶

type: Bool default: false 启用 cases 样式检查器

linter.style.cdot¶

type: Bool default: false 启用 cdot 样式检查器

linter.style.docString¶

type: Bool default: false 启用文档字符串样式检查器

linter.style.dollarSyntax¶

type: Bool default: false 启用 dollarSyntax 样式检查器

linter.style.header¶

type: Bool default: false 启用标题样式检查器

linter.style.lambdaSyntax¶

type: Bool default: false 启用 lambdaSyntax 样式检查器

linter.style.longFile¶

type: Nat default: 0 启用长文件检查器

linter.style.longFileDefValue¶

type: Nat default: 1500 每个文件行数的软性上限

linter.style.longLine¶

type: Bool default: false 启用长行检查器

linter.style.missingEnd¶

type: Bool default: false 启用缺失 end 检查器

linter.style.multiGoal¶

type: Bool default: false 启用多目标检查器

linter.style.nameCheck¶

type: Bool default: true 启用 nameCheck 检查器

linter.style.openClassical¶

type: Bool default: false 启用 openClassical 检查器

linter.style.refine¶

type: Bool default: false 启用 refine 检查器

linter.style.setOption¶

type: Bool default: false 启用 setOption 检查器

linter.suspiciousUnexpanderPatterns¶

type: Bool default: true 启用“可疑未展开模式”检查器

linter.toAdditiveExisting¶

type: Bool default: true 由 @[to_additive] 使用的检查器，验证用户是否正确指定加法声明已存在

linter.toAdditiveGenerateName¶

type: Bool default: true 由 @[to_additive] 使用的检查器，检查是否自动生成用户指定名称

linter.toAdditiveReorder¶

type: Bool default: true 检查 reorder 属性未被手动指定的检查器

linter.unnecessarySeqFocus¶

type: Bool default: true 启用 '不必要的 <;>' 检查器

linter.unnecessarySimpa¶

类型: Bool

默认值: true

启用 '不必要的 simpa' 检查器

linter.unreachableTactic¶

Lean.Elab.Tactic.BVDecide 策略使用的 SAT 求解器名称。

 1. 若设置为非空字符串，则使用该二进制文件

 2. 若设置为空字符串，将检查执行程序旁是否存在 cadical 二进制文件。通常该程序为 `lean`，我们确实在其旁附带了一个 `cadical`

 3. 若未找到，尝试从 PATH 调用 `cadical`。空字符串默认表示使用随 Lean 附带的求解器

says.no_verify_in_CI¶

type: Bool

default: false

禁用重新验证，即使 CI 环境变量已设置

says.verify¶

type: Bool

default: false

验证输出

server.reportDelayMs¶

type: Nat

type: Bool

default: true

(server) 在命令精化期间捕获 Lean stderr 通道的输出（如来自 dbg_trace 的输出）作为诊断消息

type: Bool

default: false

(trace) 启用/禁用对指定模块及其子模块的跟踪