From 97f5ad78045e52a54d12af19d93a604ceea8092f Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Wed, 11 Oct 2023 17:59:03 +1100
Subject: [PATCH] chore: change trustCompiler axiom to True (#2662)

---
 src/Init/Core.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index a14aea7316..f9899767cf 100644
--- 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`.