Skip to content

Commit beee4b9

Browse files
[lean backend] Make the extraction import the prelude by default
1 parent d5e44d3 commit beee4b9

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

rust-engine/src/main.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -38,8 +38,8 @@ fn main() {
3838
.intersperse(
3939
vec![
4040
"-- Experimental lean backend for Hax",
41-
"-- Uncomment the following line to use the prelude (requires the Lib.lean file) : ",
42-
"-- import Lib",
41+
"-- Comment the following line to not import the prelude (requires the Lib.lean file) : ",
42+
"import Lib",
4343
],
4444
allocator.hardline(),
4545
)

0 commit comments

Comments
 (0)