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

chore: remove compiler.enableNew=true from a test and rename it (#9247)

Browse source
This commit is contained in:
Cameron Zwarich 2025-07-07 22:49:57 -07:00 • committed by GitHub
parent 97fd75c660
commit 6de68dd8ef
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
tests/lean/run/opaqueNewCodeGen.lean → tests/lean/run/opaqueCodeGen.lean
View file

@ -1,7 +1,5 @@
import Lean
set_option compiler.enableNew true
/--
trace: [Compiler.result] size: 1
def f x : Nat :=
@ -15,7 +13,7 @@ opaque f : Nat → Nat :=
/--
trace: [Compiler.result] size: 0
def g a._@.opaqueNewCodeGen._hyg.1 a._@.opaqueNewCodeGen._hyg.2 : Nat :=
def g a._@.opaqueCodeGen._hyg.1 a._@.opaqueCodeGen._hyg.2 : Nat :=
extern
-/
#guard_msgs in