diff options
Diffstat (limited to '')
| -rw-r--r-- | README.md | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -83,9 +83,9 @@ to display a detailed documentation. Files generated by the Lean backend import the `Base` package from Aeneas. To use those files in Lean, create a new Lean package using `lake new`, overwrite the `lean-toolchain` with the one inside `./backends/lean`, -and add `Base` as a dependency in the `lakefile.lean`: +and add `base` as a dependency in the `lakefile.lean`: ``` -require Base from "PATH_TO_AENEAS_REPO/backends/lean" +require base from "PATH_TO_AENEAS_REPO/backends/lean" ``` ## Targeted Subset And Current Limitations |