Documentation
Lean
.
ErrorExplanations
Search
return to top
source
Imports
Lean.ErrorExplanations.CtorResultingTypeMismatch
Lean.ErrorExplanations.DependsOnNoncomputable
Lean.ErrorExplanations.InductiveParamMismatch
Lean.ErrorExplanations.InductiveParamMissing
Lean.ErrorExplanations.InferBinderTypeFailed
Lean.ErrorExplanations.InferDefTypeFailed
Lean.ErrorExplanations.InvalidDottedIdent
Lean.ErrorExplanations.ProjNonPropFromProp
Lean.ErrorExplanations.PropRecLargeElim
Lean.ErrorExplanations.RedundantMatchAlt
Lean.ErrorExplanations.UnknownIdentifier
Imported by