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

fix: test

Browse source
This commit is contained in:
Leonardo de Moura 2021-02-18 16:54:45 -08:00
parent 0a280793c7
commit c06ca8304d
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
tests/lean/run/simp1.lean
View file

@ -46,7 +46,8 @@ def tst2 : MetaM Unit := do
let s ← Meta.getSimpLemmas
let m ← s.post.getMatch lhs
trace[Meta.debug]! "result: {m}"
assert! m.size == 3
assert! m.any fun s => s.name? == `ex2
set_option trace.Meta.debug true in
#eval tst2