Error Explanations
This section provides explanations of errors and warnings that may be generated
by Lean when processing a source file. All error names listed below have the
lean package prefix.
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 | |
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 uninferrable expected type. | 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 resolve identifier to variable or constant. | Error | 4.23.0 |