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

chore: fix tests

Browse source
This commit is contained in:
Leonardo de Moura 2022-09-10 15:04:06 -07:00
parent a03ea65d73
commit 59b4d977b5
2 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
tests/lean/CompilerFindJoinPoints.lean.expected.out
View file

@ -1,3 +1,4 @@
[Compiler.test] Starting wrapper test findJoinPointsSizeLeq for findJoinPoints occurence 0
[Compiler.test] Wrapper test findJoinPointsSizeLeq for findJoinPoints occurence 0 successful
[Compiler.test] Starting post condition test findJoinPointsFix for findJoinPoints occurence 0

2
tests/lean/run/inlineApp.lean
View file

@ -10,7 +10,7 @@ def h (x : Nat) :=
open Lean Compiler LCNF in
@[cpass] def simpInline : PassInstaller :=
Testing.assertDoesNotContainConstAfter `simp `simpInlinesInline ``inline "simp did not inline `inline`"
Testing.assertDoesNotContainConstAfter ``inline "simp did not inline `inline`" |>.install `simp `simpInlinesInline
set_option trace.Compiler.result true
#eval Lean.Compiler.compile #[``h]