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 | |
Dotted identifier notation used with invalid or uninferrable expected type. | Error | 4.22.0 | |
Match alternative will never be reached. | Error | 4.22.0 |
