chore: change trustCompiler axiom to True

2026-03-19 11:24:07 +00:00 · 2023-10-11 16:45:25 +11:00
1 changed files with 1 additions and 1 deletions
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -1615,7 +1615,7 @@ namespace Lean
 /--
 Depends on the correctness of the Lean compiler, interpreter, and all `[implemented_by ...]` and `[extern ...]` annotations.
 -/
-axiom trustCompiler : False
+axiom trustCompiler : True

 /--
 When the kernel tries to reduce a term `Lean.reduceBool c`, it will invoke the Lean interpreter to evaluate `c`.