Skip to content

Commit

Permalink
fix: forgot an assignation
Browse files Browse the repository at this point in the history
  • Loading branch information
arthur-adjedj authored and semorrison committed Jul 25, 2024
1 parent acb4721 commit 9416d0f
Showing 1 changed file with 1 addition and 0 deletions.
1 change: 1 addition & 0 deletions src/Lean/Elab/Deriving/BEq.lean
Original file line number Diff line number Diff line change
Expand Up @@ -73,6 +73,7 @@ where
cases (eq_of_beq h)
exact $rhs
else false)
rhs_empty := false
else
if rhs_empty then
rhs ← `($a:ident == $b:ident)
Expand Down

0 comments on commit 9416d0f

Please sign in to comment.