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

chore: change trustCompiler axiom to True (#2662)

Browse source
This commit is contained in:
Scott Morrison 2023-10-11 17:59:03 +11:00 • committed by GitHub
parent 115991066d
commit 97f5ad7804
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Core.lean
View file

@ -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`.