Skip to content

Commit 6063d9d

Browse files
committed
chore: fix bug in pattern match of Expr
1 parent 4b44ee9 commit 6063d9d

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

src/Lean/Elab/Tactic/BVAckermannize.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -53,8 +53,8 @@ with `?w` a literal `Nat`. -/
5353
def ofExpr? (e : Expr) : MetaM (Option BVTy) := ofExpr?Aux e |>.run where
5454
ofExpr?Aux (e : Expr) : OptionT MetaM BVTy :=
5555
match_expr e.consumeMData with
56-
| bool => return bool
57-
| bitVec w => do
56+
| Bool => return bool
57+
| BitVec w => do
5858
let w ← getNatValue? w
5959
return bitVec w
6060
| _ => OptionT.fail

0 commit comments

Comments
 (0)