From bd21583d4bdffd926a51e15c8d3fb0f73e7a4e61 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 7 Sep 2022 20:35:59 -0700
Subject: [PATCH] fix: `ComputedFields.lean`

`all` fields was not being set correctly.
TODO: check `all` fields in the kernel.
---
 src/Lean/Elab/ComputedFields.lean | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Elab/ComputedFields.lean b/src/Lean/Elab/ComputedFields.lean
index f07f4f23b3..0f8299e38d 100644
--- a/src/Lean/Elab/ComputedFields.lean
+++ b/src/Lean/Elab/ComputedFields.lean
@@ -108,10 +108,12 @@ def overrideCasesOn : M Unit := do
           forallTelescope (← inferType minor) fun args _ => do
             mkLambdaFVars ((if ← isScalarField ctor then #[] else compFieldVars) ++ args)
               (← mkUnsafeCastTo constMotive (mkAppN minor args)))
+  let nameOverride := mkCasesOnName name ++ `_override
   addDecl <| .defnDecl { casesOn with
-    name := mkCasesOnName name ++ `_override
+    name := nameOverride
+    all  := [nameOverride]
     value
-    hints := .opaque
+    hints  := .opaque
     safety := .unsafe
   }
   setInlineAttribute (mkCasesOnName name ++ `_override)