The Lean Language Reference

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

ctor­Resulting­Type­Mismatch

Resulting type of constructor was not the inductive type being declared.

Error

4.22.0

depends­On­Noncomputable

Declaration depends on noncomputable definitions but is not marked as noncomputable

Error

4.22.0

inductive­Param­Mismatch

Invalid parameter in an occurrence of an inductive type in one of its constructors.

Error

4.22.0

inductive­Param­Missing

Parameter not present in an occurrence of an inductive type in one of its constructors.

Error

4.22.0

infer­Binder­Type­Failed

The type of a binder could not be inferred.

Error

4.23.0

infer­Def­Type­Failed

The type of a definition could not be inferred.

Error

4.23.0

invalid­Dotted­Ident

Dotted identifier notation used with invalid or uninferrable expected type.

Error

4.22.0

proj­Non­Prop­From­Prop

Tried to project data from a proof.

Error

4.23.0

prop­Rec­Large­Elim

Attempted to eliminate a proof into a higher type universe.

Error

4.23.0

redundant­Match­Alt

Match alternative will never be reached.

Error

4.22.0

unknown­Identifier

Failed to resolve identifier to variable or constant.

Error

4.23.0