The Lean Language Reference

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.

"failed to compile 'partial' definition" on meta definition

This can happen when a definition with a type that is not known to be Nonempty is marked meta or moved into a meta section, which both imply partial without a termination metric. Use termination_by? to make the previously implicitly inferred termination metric explicit, or provide a Nonempty instance.

Recipe for Porting Existing Files

Start by enabling the module system throughout all files with minimal breaking changes:

  • Prefix all files with module.

  • Make all existing imports public unless you know they will be used only in proofs. Add import all when getting errors about references to private data. Add public meta import when getting "must be meta" errors (public may be avoided when defining local-only metaprograms).

  • Prefix the remainder of the file with @[expose] public section or, for programming-focused files, with public section.

After getting an initial build under the module system to work, you can then work iteratively on minimizing uses of public and @[expose] where sensible.