Skip to content

Commit 817ae29

Browse files
committed
swap tactics used to solve matchbv goal
1 parent 6c89592 commit 817ae29

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/sail_lean_backend/Sail/BitVec.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -228,7 +228,7 @@ def elabMatchBv : TermElab := fun stx typ? =>
228228
if let some rhsElse := rhsElse? then
229229
`(Function.const _ $rhsElse)
230230
else
231-
`(fun _ => by try grind; try bv_decide)
231+
`(fun _ => by try bv_decide; try grind)
232232

233233
for ps in pss.reverse, rhs in rhss.reverse do
234234
let test ← genBVPatMatchTest xs ps

0 commit comments

Comments
 (0)