Common Errors and Patterns

The following list contains common errors one might encounter when using the module system and especially porting existing files to the module system.

Unknown constant

Check whether you might be trying to access a private definition in the public scope. If so, you might want to make the current declaration private as well or otherwise enter the private scope such as through private on a field or by for a proof. TODO: improve error message.

If the message is prefixed with (interpreter), this suggests a missing meta import. The new import should be placed in the file defining the metaprogram depending on the missing constant, which is not necessarily the file triggering the error. Note that the language server always does meta imports for the benefit of #eval etc., so the error might only occur in a cmdline build. TODO: better, static meta checking.

Definitional equality errors, especially after porting

You are likely missing an expose attribute on a definition or alternatively, if imported, an import all. Prefer the former if anyone outside your library might feasible require the same access. Lean.reduceCmd : command`#reduce <expression>` reduces the expression `<expression>` to its normal form. This involves applying reduction rules until no further reduction is possible. By default, proofs and types within the expression are not reduced. Use modifiers `(proofs := true)` and `(types := true)` to reduce them. Recall that propositions are types in Lean. **Warning:** This can be a computationally expensive operation, especially for complex expressions. Consider using `#eval <expression>` for simple evaluation/execution of expressions. #reduce and/or trace.Meta.isDefEq can help with finding the blocking definition. You might also see this as a kernel error when a tactic directly emits proof terms referencing specific declarations without going through the elaborator, such as for proof by reflection. In this case, there is no readily available trace for debugging; consider using @[expose] sections generously on the closure of relevant modules.