Lean 4 标准库开发指南命名约定、风格规范与项目愿景【免费下载链接】lean4Lean 4 programming language and theorem prover项目地址: https://gitcode.com/GitHub_Trending/le/lean4本指南基于 Lean 4 官方仓库中 doc/std 目录下的标准库开发文档系统梳理 Lean 标准库的定位与愿景、命名约定与命名算法、代码风格规范以及社区贡献流程。读完本文你将掌握如何为 Lean 标准库中的类型、数据与定理选择规范名称如何写出符合官方风格指南的 Lean 代码以及如何参与标准库的演进与贡献。说明面向 Lean 标准库用户的 API 文档属于 Lean 语言参考Lean Language Reference的一部分doc/std/目录下的三份文档 vision.md愿景与贡献指南、style.md风格指南与 naming.md命名约定则专门面向标准库的开发者与贡献者。一、Lean 4 标准库的定位与愿景1.1 什么是 Lean 标准库Lean 4 标准库是 Lean 发行版的核心组成部分为函数式编程、可信软件开发和软件验证提供基础构件。与大多数语言的标准库不同Lean 标准库的许多组件都经过形式化验证可以直接作为验证应用的一部分使用见 vision.md。需要特别注意的是标准库是一个公共 API 概念并不与源码仓库中的某个具体目录如Std一一对应。例如元编程框架metaprogramming framework不属于标准库而True、Nat这类基础类型属于标准库。标准库的维护团队按字母序为Henrik Böving、Markus Himmel社区联络与外部贡献协调人、Kim Morrison、Paul Reichert、Sofia Rodrigues主要由 Lean FRO 主导开发。1.2 六条指导原则标准库目前处于活跃开发状态其指导原则是为真实世界的软件提供全面、经过验证的构件构建一个内部一致性极佳的、最高质量的公共 API仔细优化可能用于性能敏感型软件的组件确保用户平滑的采纳与维护体验提供优秀的文档、示例项目与指南为软件开发、软件验证和数学库提供可靠且可扩展的基础。1.3 标准库内容大纲标准库覆盖以下范围详见 vision.md 的 Standard library outline大类子类1. 核心类型与操作基础类型数值类型含浮点数容器字符串与格式化2. 语言构造范围与迭代器比较、排序、哈希及相关类型类基础单子基础设施3. 库随机数日期与时间4. 操作系统抽象并发与并行原语异步 I/OFFI 辅助环境、文件系统、进程区域设置其中前三节的内容核心类型与操作、语言构造、库原则上都会经过形式化验证例外是浮点数以及与操作系统交互的库部分如操作系统随机数来源、时区数据库访问等。这一验证承诺与源码仓库中标准库源码的分布相对应核心基础类型位于 src/Init标准库扩展位于 src/Std例如容器、时间等见下文 grove 大纲文件的结构划分。二、标准库命名约定让名字可被猜中命名约定文档 开宗明义地指出标准库中访问一个结果最便捷的方式是正确猜出声明的名字可借助标识符自动补全。因此易猜且足够短的名字能显著提升 Lean 使用者的效率。整份指南硬规则极少、启发式很多、示例精选——它无法也无意给出一个在所有情况下都能选出好名字的确定性算法而是一份随着代码评审不断澄清与扩充的活文档。2.1 三种大小写类型、数据、定理标识符混合使用三种命名风格分别用于类型、数据与定理类型codomain 为Sort u的可能 0 元的函数使用UpperCamelCase如List、List.IsPrefix数据codomain 不是Sort u而是某个Type u的可能 0 元的函数使用lowerCamelCase如List.append、List.isPrefixOf定理使用snake_case。定义谓词时以Is作为前缀如List.IsPrefix。以下情况可以省略Is前缀结果名字不符合语法习惯谓词依赖额外数据加Is会造成混淆如List.Pairwise名字本身是形容词如Std.Time.Month.Ordinal.Valid。结构体字段的命名应使投影projection具有正确的名字。2.2 命名空间与广义投影记号几乎总是应该将与某类型相关的定义和定理放入与类型同名的命名空间中关于列表的操作与定理放在List命名空间中关于Std.Time.PlainDate的操作与定理放在Std.Time.PlainDate命名空间中。根命名空间的声明相对罕见最常见的是关于记号类型类导出的数据与性质、且不针对实现该类型类的具体类型的声明例如theorem beq_iff_eq [BEq α] [LawfulBEq α] {a b : α} : a b ↔ a b : sorry而下面的定理属于List命名空间theorem List.cons_beq_cons [BEq α] {a b : α} {l₁ l₂ : List α} : (a :: l₁ b :: l₂) (a b l₁ l₂) : rfl当多个命名空间交织时一般原则是把定理放在出现在其假设之一中的最具体的命名空间。下面两个名字都符合约定theorem List.Sublist.reverse : l₁ l₂ → l₁.reverse l₂.reverse : sorry theorem List.reverse_sublist : l₁.reverse l₂.reverse ↔ l₁ l₂ : sorry注意第二个定理没有任何形如List.Sublist l的假设因此List.Sublist.reverse_iff这个名字是错误的。把结果放在List.Sublist这类命名空间的好处是启用广义投影记号generalized projection notation给定h : l₁ l₂可以直接写h.reverse得到l₁.reverse l₂.reverse的证明。思考哪些点记号dot notation写起来方便可以作为决定定理放置位置的准则偶尔也是把同一定理复制到多个命名空间的正当理由。关于Std命名空间新增类型通常放在Std命名空间与Std/源码目录中除非有充分的理由放在别处。在Std命名空间内部所有内部声明应为private或者包含一个明确标记其内部性质的名字成分最好使用Internal。这一要求与 src/Std 目录下如 src/Std/Data/HashMap 中的Raw、Raw₀等内部实现层的分层实现风格一致——内部细节与公共 API 严格隔离。2.3 数据函数的命名定义数据时使用lowerCamelCase。如果数据在道德上完全由其类型确定morally fully specified by its type则使用下面定理的命名流程并转为小驼峰形式。对于返回Option的函数考虑加后缀?对于可能 panic 的函数考虑加后缀!。很多情况下一个函数会有多个变体一个返回Option、一个可能 panic、还可能有一个接收证明参数的版本。源码中即可看到这种惯例例如 List.isPrefixOf 与List.isPrefixOf?同时存在。2.4 定理及部分定义的命名算法理论上存在一个通用的命名算法但问题在于它会产生非常冗长笨拙的名字需要再加以缩短。因此给声明起名包含机械部分与创意部分。第一步根据上述准则决定结果所属的命名空间。第二步把声明的类型视为一棵树——内节点是函数类型或函数应用叶子是 0 元函数或绑定变量。以下面的标准库结果为例example {α : Type u} {β : Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited β] {m : Std.HashMap α β} {a : α} {h : a ∈ m} : m[a]? some (m[a]h) : sorry正确的命名空间显然是Std.HashMap对应的类型树如下记号的推荐拼写可以通过悬停在记号上查看第三步遍历这棵树按照以下规则构造名字遇到函数类型时先把结果类型转成名字再按从左到右把各参数类型转成名字用_of_连接遇到既非中缀记号也非结构投影的函数时先放函数名再放下划线连接的各参数遇到中缀记号时用记号的名字以下划线分隔连接各参数遇到结构投影时按普通函数处理但把投影名放在最后遇到名字时转成小驼峰lower camel case跳过绑定变量和证明类型类参数一般也跳过遇到命名空间名时以小驼峰形式拼接。对上面的例子应用该算法得到Std.HashMap.getElem?_eq_optionSome_getElem_of_mem第四步使用以下启发式缩短名字函数的命名空间如果从上下文明显可见或就是当前命名空间可以省略绝大多数情况如此对于中缀运算符如果 RHS或记号名加 RHS从上下文明显可见可以省略如果假设明显是必需的或出现在结论中可以省略。据此上例的候选名字包括Std.HashMap.getElem?_eqStd.HashMap.getElem?_eq_of_memStd.HashMap.getElem?_eq_someStd.HashMap.getElem?_eq_some_of_memStd.HashMap.getElem?_eq_some_getElemStd.Hashmap.getElem?_eq_some_getElem_of_mem由于还存在一个联系m[a]?与m[a]!的引理可能占用前四个名字最终前四个都欠具体后两个中更短的是第 5 个这正是 Lean 标准库中该引理的实际命名。这一命名实践可以在 src/Std/Data/HashMap 的引理文件中找到大量对应实例。更多示例与遍历顺序的影响example {x y : List α} (h : x : y) (hx : x ≠ []) : x.head hx y.head (h.ne_nil hx) : sorry因为存在IsPrefix参数该结果应位于List.IsPrefix命名空间算法建议List.IsPrefix.head_eq_head_of_ne_nil缩短为List.IsPrefix.head。注意命名空间名IsPrefix与对应记号的推荐拼写prefix是不同的。example : l₁ : l₂ → reverse l₁ : reverse l₂ : sorry同样位于List.IsPrefix命名空间算法建议List.IsPrefix.reverse_prefix_reverse缩短为List.IsPrefix.reverse。遍历顺序常常很关键例如下面两个定理theorem Nat.mul_zero (n : Nat) : n * 0 0 : sorry theorem Nat.zero_mul (n : Nat) : 0 * n 0 : sorry一个名字可能是另一个名字的前缀theorem Int.mul_ne_zero {a b : Int} (a0 : a ≠ 0) (b0 : b ≠ 0) : a * b ≠ 0 : sorry theorem Int.mul_ne_zero_iff {a b : Int} : a * b ≠ 0 ↔ a ≠ 0 ∧ b ≠ 0 : sorry即使不加iff名字也唯一通常仍建议在定理名中包含iff。例如theorem List.head?_eq_none_iff : l.head? none ↔ l [] : sorry若该引理只叫List.head?_eq_none当目标是l.head? none时用户可能尝试apply它造成困惑。期望或希望越常用的定理名字应该越短。例如标准库同时拥有theorem Std.HashMap.getElem?_eq_none_of_contains_eq_false {a : α} : m.contains a false → m[a]? none : sorry theorem Std.HashMap.getElem?_eq_none {a : α} : ¬a ∈ m → m[a]? none : sorry由于鼓励哈希表用户使用∈而非contains第二个引理获得了更短的名字。2.5 特殊关键词速查表命名约定文档给出了可能出现在标识符中的一组特殊关键词完整表格如下关键词含义示例def展开一个定义。公共 API 尽量避免Nat.max_defrefl形如a R a的定理R 是自反关系且a是显式参数Nat.le_reflrfl同refl但a为隐式Nat.le_rflirrefl形如¬a R a的定理R 是反自反关系Nat.lt_irreflsymm形如a R b → b R a的定理R 是对称关系对比下方commEq.symmtrans形如a R b → b R c → a R c的定理R 是传递关系可携带数据Eq.transantisymmm形如a R b → b R a → a b的定理R 是反对称关系Nat.le_antisymmcongr形如a R b → f a S f b的定理R 与 S 通常是等价关系Std.HashMap.mem_congrcomm形如f a b f b a的定理对比上方symmEq.comm、Nat.add_commassoc形如g (f a b) c f a (g b c)的定理注意顺序多数情况下 f gNat.add_sub_assocdistrib形如f (g a b) g (f a) (f b)的定理Nat.add_left_distribself变量在结论中多次出现时可用List.mem_cons_selfinj形如f a f b ↔ a b的定理Int.neg_inj、Nat.add_left_injcancel形如f a f b → a b或g (f a) a的定理其中 f、g 通常涉及二元运算Nat.add_sub_cancelcancel_iff同inj但左右侧约定不同见下文Nat.add_right_cancel_iffext形如f a f b → a b的定理f 通常涉及某种投影List.ext_getElemmono形如a R b → f a R f b的定理R 是传递关系List.countP_mono_left表中antisymmm为原文档笔误应为antisymm此处如实保留原文实际标准库中的惯用关键词为antisymm如Nat.le_antisymm示例所示。这些关键词在 src/Init 与 src/Std 的引理文件中大量出现例如Nat.add_comm、Nat.mul_zero与Nat.zero_mul参见 src/Init/Data/Fin/Lemmas.lean 中等价的受保护定理可作为命名惯例的活样本。Left 与 Right 的约定left与right关键词用于区分定理的对称变体theorem imp_congr_left (h : a ↔ b) : (a → c) ↔ (b → c) : sorry theorem imp_congr_right (h : a → (b ↔ c)) : (a → b) ↔ (a → c) : sorry哪一侧是left、哪一侧是right并不总是显而易见。启发式地说定理应命名更可变more variable的一侧但存在例外。对于本节讨论的部分特殊关键词有明确约定theorem Nat.left_distrib (n m k : Nat) : n * (m k) n * m n * k : sorry theorem Nat.right_distrib (n m k : Nat) : (n m) * k n * k m * k : sorry theorem Nat.add_left_cancel {n m k : Nat} : n m n k → m k : sorry theorem Nat.add_right_cancel {n m k : Nat} : n m k m → n k : sorry theorem Nat.add_left_cancel_iff {m k n : Nat} : n m n k ↔ m k : sorry theorem Nat.add_right_cancel_iff {m k n : Nat} : m n k n ↔ m k : sorry theorem Nat.add_left_inj {m k n : Nat} : m n k n ↔ m k : sorry theorem Nat.add_right_inj {m k n : Nat} : n m n k ↔ m k : sorry特别注意cancel_iff与inj的约定恰好相反。此外theorem Nat.add_sub_self_left (a b : Nat) : (a b) - a b : sorry theorem Nat.add_sub_self_right (a b : Nat) : (a b) - b a : sorry theorem Nat.add_sub_cancel (n m : Nat) : (n m) - m n : sorry2.6 素数命名、缩略词与 simp 集合避免用字符区分概念的变体例如同时引入BitVec.sshiftRight与BitVec.sshiftRight不查看类型签名、文档甚至代码就无法区分二者即便知道有两种变体也无从得知哪个是哪个。应优先采用描述性配对如BitVec.sshiftRightNat/BitVec.sshiftRight。缩略词三个字母及以内的缩略词所有字母遵循相应命名风格的大小写如IO是正确的类型名IO.Ref在定义名中可写作IORef在定理名中写作ioRef至少四个字母的缩略词从第二个字母开始切换为小写如Json与JsonRPC都是正确的类型名如果缩略词通常以混合大小写拼写可以在标识符中沿用如Std.Net.IPv4Addr。Simp 集合围绕某个转换函数的 simp 集合命名为source_to_target。例如服务于BitVec.toNat从BitVec到Nat的 simp 集合应命名为bitvec_to_nat。2.7 变量命名建议以下是推荐但不强制的变量命名简单假设命名为h、h或使用数字序列h₁、h₂等另一种常见名是wwitness见证List命名为l、l、l₁等或as、bs等列表类型不同时鼓励用as/bs如as : List α与bs : List βxs、ys、zs允许但最好保留给Array与Vector列表的列表可命名为LArray命名为xs、ys、zs类型不同时鼓励as/bs数组的数组可命名为xssVector同样命名为xs、ys、zs类型不同时鼓励as/bs如as : Vector α n与bs : Vector β n向量的向量可命名为xssList/Array/Vector的常见例外递归函数中的累加器使用acc数值索引优先用i、j、k能提高可读性时鼓励描述性名字如start、stop、lo、hi尺寸优先用n、m例如Vector α n或xs.size nBitVec的宽度优先用w。三、标准库代码风格指南风格指南 提醒贡献者Lean 编译器不会强制格式规则但一致格式的代码更易读、更易维护——对格式的讲究不仅是外观问题它反映的是达到 Lean 4 标准库深层标准所需的同样水平的精确与用心。风格指南仅适用于 Lean 标准库尽管部分示例取自 Lean 代码库的其他部分。3.1 基础空白规则语法元素如:、:、|、::两侧各留一个空格例外是,与;其后留空格、前不留分隔符如()、{}内侧不留空格例外是子类型记号与结构实例记号。正确的函数参数示例{α : Type u} [BEq α] (cmp : α → α → Ordering) (hab : a b) {d : { l : List ((n : Nat) × Vector Nat n) // l.length % 2 0 }}正确的项示例1 :: [2, 3] letI : Ord α : ⟨cmp⟩; True (⟨2, 3⟩ : Nat × Nat) ((2, 3) : Nat × Nat) { x with fst : f (4 f 0), snd : 4, .. } match 1 with | 0 0 | _ 0 fun ⟨a, b⟩ _ _ by cases hab ; apply id; rw [hbc]配置编辑器去除行尾空白按推荐方式配置 Visual Studio Code 进行 Lean 开发时该设置会自动生效。3.2 跨行拆分规则跨行拆分项时从第二行开始缩进增加两个空格拆分函数应用时尽量在参数边界处拆分参数本身需要拆分时再适当增加缩进在中缀运算符处拆分时运算符放在第一行末尾而非第二行开头是否加深缩进取决于可读性拆分if-then-else时then与条件同行、else与分支项同行否则按if/else作为同一函数参数的方式缩进拆分逗号分隔的括号序列匿名构造器应用、列表/数组/向量字面量、元组时后续行可对齐也可缩进两个空格不要让括号孤立Do not orphan parentheses。正确示例def MacroScopesView.isPrefixOf (v₁ v₂ : MacroScopesView) : Bool : v₁.name.isPrefixOf v₂.name v₁.scopes v₂.scopes v₁.mainModule v₂.mainModule v₁.imported v₂.importedtheorem eraseP_eq_iff {p} {l : List α} : l.eraseP p l ↔ ((∀ a ∈ l, ¬ p a) ∧ l l) ∨ ∃ a l₁ l₂, (∀ b ∈ l₁, ¬ p b) ∧ p a ∧ l l₁ a :: l₂ ∧ l l₁ l₂ : sorry3.3 文件结构与顶层声明每个文件应依次包含版权头、导入标准库中始终包含prelude声明和模块文档字符串版权头与导入之间不留空行导入与模块文档字符串之间留空行。显式声明宇宙变量时放在模块文档之后、文件顶部/- Copyright (c) 2014 Parikshit Khanna. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro, Yury Kudryashov -/ prelude import Init.Data.List.Pairwise import Init.Data.List.Find /-! **# Lemmas about List.eraseP and List.erase.** -/ universe u u不面向用户的语法必须限定作用域scoped新的公共语法必须显式地在 RFC 中讨论。其他顶层规则所有顶层命令不缩进section、namespace等分区命令不增加缩进层级属性可与命令同行也可单独一行多行声明头从第二行起缩进四个空格声明类型的冒号不能放在行首或独占一行声明体缩进两个空格较短的声明体可与声明类型同行。[simp] theorem eraseP_nil : [].eraseP p [] : rfl或[simp] theorem eraseP_nil : [].eraseP p [] : rfl3.4 文档注释docstring声明应按docBlamelinter 的要求编写文档可在文件中用set_option linter.missingDocs true激活允许保留该选项单行文档注释与/--、-/同行多行文档字符串的分隔符独占一行文档注释本身不缩进文档注释必须使用陈述语气indicative mood并使用美式拼写。正确示例单行/-- Carries out a monadic action on each mapping in the hash map in some order. -/ [inline] def forM (f : (a : α) → β a → m PUnit) (b : Raw α β) : m PUnit : b.buckets.forM (AssocList.forM f)正确示例多行/-- Monadically computes a value by folding the given function over the mappings in the hash map in some order. -/ [inline] def foldM (f : δ → (a : α) → β a → m δ) (init : δ) (b : Raw α β) : m δ : b.buckets.foldlM (fun acc l l.foldlM f acc) init3.5where子句、终止参数与derivingwhere关键字不缩进其绑定的声明缩进两个空格where前后及where内部声明之间的空行可选以可读性为准termination_by、decreasing_by、partial_fixpoint关键字不缩进相关项按声明体的方式缩进deriving子句不缩进。structure Iterator where array : ByteArray idx : Nat deriving Inhabited3.6 记号与 Unicode标准库倾向使用已有记号且通常优先使用 Unicode 版本而非非 Unicode 替代。具体规则与例外Sigma 类型使用(a : α) × β a而非Σ a, β a或Sigma β函数箭头使用fun a f x而非fun x ↦ f x、λ x f x或任何其他变体。3.7 模式匹配、结构体与结构声明match 分支缩进到match 语句独占一行时的缩进层级若 match 是隐式的分支按显式给出 match 的方式缩进分支内容缩进两个空格使其与 match 模式处于同一层级match 分支的对齐允许但不强制多行结构实例语法左花括号在前一行行尾右花括号独占一行其余语法缩进一层结构更新时with子句与左花括号同行在赋值符号处对齐允许但不强制定义结构类型时不要给结构字段加括号使用自定义构造器名声明结构时把自定义名字放在单独一行、像结构字段一样缩进并添加文档注释。/-- A bitvector of the specified width. This is represented as the underlying Nat number in both the runtime and the kernel, inheriting all the special support for Nat. -/ structure BitVec (w : Nat) where /-- Constructs a BitVec w from a number less than 2^w. O(1), because we use Fin as the internal representation of a bitvector. -/ ofFin :: /-- Interprets a bitvector as a number less than 2^w. O(1), because we use Fin as the internal representation of a bitvector. -/ toFin : Fin (2 ^ w)3.8 Tactic 证明与do记号Tactic 证明是各类升级中最容易破裂的部分因此要用最小化破坏概率、便于调试的方式编写多目标时使用 tactic 组合子如all_goals作用于全部或明确指定的子集或用焦点圆点focus dots逐个处理鼓励使用结构化证明如induction … with但不强制挤压非终结simp即未关闭目标的simp一般不建议挤压终结simp除非挤压带来明显性能提升不要过度 golf 证明避免复杂的多目标组合子操作、复杂的替换运算符▸用法、精巧的无点表达式等难以调试的写法也不要欠 golf常规任务使用最强大的可用 tactic不使用erw避免在simp或rw之后使用rfl这通常说明缺少一个本应使用的引理用(d)simp或rw代替delta或unfold用refine而非refine仅在确实需要时使用haveI和letI**优先使用高度自动化的 tactic如grind、omega**而非底层证明除非自动 tactic 需要不可接受的额外导入或性能不佳若决定不用自动 tactic应加注释说明原因。do记号方面do关键字与对应的:或等同行Id.run do视同裸do使用提前return减少嵌套深度让函数的非异常控制流更清晰let匹配的备选分支可放在同行或下一行缩进两个空格若被匹配项本身跨多行且有备选分支考虑在←之后立即断行并按可读性需要缩进。def getFunDecl (fvarId : FVarId) : CompilerM FunDecl : do let some decl ← findFunDecl? fvarId | throwError unknown local function {fvarId.name} return decl四、标准库 QAGrove 数据文件doc/std/grove 目录存放标准库的Grove数据文件用于标准库的质量保障QA。其结构直接对应 vision.md 中的标准库大纲GroveStdlib/Std/CoreTypesAndOperations/基础类型、数值、容器、字符串与格式化GroveStdlib/Std/LanguageConstructs/比较/排序/哈希、单子、范围与迭代器GroveStdlib/Std/Libraries/日期与时间、随机数GroveStdlib/Std/OperatingSystemAbstractions/异步 I/O、基础 I/O、并发与并行、环境/文件系统/进程、区域设置GroveStdlib/Generated/自动生成的覆盖性检查文件如 associative 系列操作覆盖、创建-查询/修改-查询等场景。这些文件以机器可读的方式跟踪大纲各条目配合目录下的lakefile.toml、lean-toolchain与update_invalidated.sh等脚本构成标准库覆盖度与一致性检查的基础设施。五、如何为 Lean 标准库做贡献愿景文档 的 Call for contributions 明确了两条社区贡献路径路径一提交使用经验报告。如果你正在用 Lean 做软件验证或可信软件开发向我们分享你的使用体验非常有价值。可以直接通过 Zulip#lean4 频道的公开话题或私信联系维护团队哪怕是提供一个代码链接也很有帮助。这些反馈会直接影响标准库面向真实应用场景的持续演进。路径二提交代码与引理。如果你认为某段代码能增强标准库建议先在 Zulip 的 #lean4 频道发起讨论这是获得初步反馈最有效的方式。标准库的范围非常精确、质量标准非常高目前主要欢迎扩充已有材料的贡献而非引入全新概念。如果你愿意贡献但不知道做什么直接联系维护团队如 Markus Himmel总有适合新贡献者的有意义的工作。按照 CONTRIBUTING.md 中的项目级外部贡献指南在 RFC 之后提交、或先与标准库维护团队成员讨论过计划的 PR 被合并的概率要高得多拿不准时先做个自我介绍总是好的。此外标准库中的所有代码都严格遵循标准库编码约定即本文第三节的 style.md与命名约定本文第二节的 naming.md。结语Lean 4 标准库既是 Lean 发行版的核心构件也是一项持续进化的工程。doc/std/下的三份文档从愿景vision.md、风格style.md与命名naming.md三个维度为贡献者划定了清晰的边界与路径命名以可被猜中为目标通过类型树遍历算法加启发式缩短来生成规范名称风格以一致与精确为标尺覆盖空白、拆分、文件结构、文档注释、tactic 证明与do记号等方方面面愿景则以经过验证的、面向真实世界的公共 API为方向配合 Grove QA 数据与开放贡献渠道持续演进。无论你是想为标准库提交第一个引理还是希望深入理解其内部一致性这份指南都是你的起点。【免费下载链接】lean4Lean 4 programming language and theorem prover项目地址: https://gitcode.com/GitHub_Trending/le/lean4创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考