错误说明
本节说明 Lean 处理源文件时可能生成的错误和警告。下面列出的所有错误名称都带有
lean 包前缀。
名称 | 摘要 | 严重性 | 版本 |
|---|---|---|---|
Resulting type of constructor was not the inductive type being declared. | 错误 | 4.22.0 | |
Declaration depends on noncomputable definitions but is not marked as noncomputable | 错误 | 4.22.0 | |
Induction pattern with nontactic in natural-number-game-style `with` clause. | 错误 | 4.26.0 | |
Invalid parameter in an occurrence of an inductive type in one of its constructors. | 错误 | 4.22.0 | |
Parameter not present in an occurrence of an inductive type in one of its constructors. | 错误 | 4.22.0 | |
The type of a binder could not be inferred. | 错误 | 4.23.0 | |
The type of a definition could not be inferred. | 错误 | 4.23.0 | |
Dotted identifier notation used with invalid or non-inferrable expected type. | 错误 | 4.22.0 | |
Generalized field notation used in a potentially ambiguous way. | 错误 | 4.22.0 | |
Tried to project data from a proof. | 错误 | 4.23.0 | |
Attempted to eliminate a proof into a higher type universe. | 错误 | 4.23.0 | |
Match alternative will never be reached. | 错误 | 4.22.0 | |
Failed to synthesize instance of type class. | 错误 | 4.26.0 | |
Failed to resolve identifier to variable or constant. | 错误 | 4.23.0 |