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