From a04f3cab5a9fe2870825af6544ca13c5bb766706 Mon Sep 17 00:00:00 2001 From: arthur-adjedj Date: Sat, 29 Jun 2024 13:05:36 +0200 Subject: [PATCH] fix: reduction behaviour of derived `BEq` instances fix: forgot an assignation --- src/Lean/Elab/Deriving/BEq.lean | 16 +++++++++++++--- 1 file changed, 13 insertions(+), 3 deletions(-) diff --git a/src/Lean/Elab/Deriving/BEq.lean b/src/Lean/Elab/Deriving/BEq.lean index 81ffdb70ca..5e9cb3cc5b 100644 --- a/src/Lean/Elab/Deriving/BEq.lean +++ b/src/Lean/Elab/Deriving/BEq.lean @@ -43,6 +43,7 @@ where let mut ctorArgs1 := #[] let mut ctorArgs2 := #[] let mut rhs ← `(true) + let mut rhs_empty := true for i in [:ctorInfo.numFields] do let pos := indVal.numParams + ctorInfo.numFields - i - 1 let x := xs[pos]! @@ -59,17 +60,26 @@ where if (← isProp xType) then continue if xType.isAppOf indVal.name then - rhs ← `($(mkIdent auxFunName):ident $a:ident $b:ident && $rhs) + if rhs_empty then + rhs ← `($(mkIdent auxFunName):ident $a:ident $b:ident) + rhs_empty := false + else + rhs ← `($(mkIdent auxFunName):ident $a:ident $b:ident && $rhs) /- If `x` appears in the type of another field, use `eq_of_beq` to unify the types of the subsequent variables -/ else if ← xs[pos+1:].anyM - (fun fvar => (Lean.Expr.containsFVar · x.fvarId!) <$> (inferType fvar)) then + (fun fvar => (Expr.containsFVar · x.fvarId!) <$> (inferType fvar)) then rhs ← `(if h : $a:ident == $b:ident then by cases (eq_of_beq h) exact $rhs else false) + rhs_empty := false else - rhs ← `($a:ident == $b:ident && $rhs) + if rhs_empty then + rhs ← `($a:ident == $b:ident) + rhs_empty := false + else + rhs ← `($a:ident == $b:ident && $rhs) -- add `_` for inductive parameters, they are inaccessible for _ in [:indVal.numParams] do ctorArgs1 := ctorArgs1.push (← `(_))