max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: enable the new compiler

Browse source
This commit is contained in:
Cameron Zwarich 2025-06-14 07:41:27 -07:00 • committed by Joachim Breitner
parent a8d5982fce
commit 7f8ccd8425
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/CoreM.lean
View file

@ -667,9 +667,9 @@ private def checkUnsupported [Monad m] [MonadEnv m] [MonadError m] (decl : Decla
| _ => pure ()
register_builtin_option compiler.enableNew : Bool := {
defValue := false
defValue := true
group := "compiler"
descr := "(compiler) enable the new code generator, this should have no significant effect on your code but it does help to test the new code generator; unset to only use the old code generator instead"
descr := "(compiler) enable the new code generator, unset to use the old code generator instead"
}
/--