From f6e88e5a0525b744c5df018dd96d2f0cbca29435 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Wed, 4 Dec 2024 20:49:16 +0100
Subject: [PATCH] fix: missing `HEq` support at `ToLCNF` (#6311)

This PR adds support for `HEq` to the new code generator.
---
 src/Lean/Compiler/LCNF/ToLCNF.lean | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/src/Lean/Compiler/LCNF/ToLCNF.lean b/src/Lean/Compiler/LCNF/ToLCNF.lean
index fc5408c3a1..791d914c32 100644
--- a/src/Lean/Compiler/LCNF/ToLCNF.lean
+++ b/src/Lean/Compiler/LCNF/ToLCNF.lean
@@ -593,6 +593,14 @@ where
       let minor ← visit minor
       mkOverApplication minor args arity
 
+  visitHEqRec (e : Expr) : M Arg :=
+    let arity := 7
+    etaIfUnderApplied e arity do
+      let args := e.getAppArgs
+      let minor := if e.isAppOf ``HEq.rec || e.isAppOf ``HEq.ndrec then args[3]! else args[6]!
+      let minor ← visit minor
+      mkOverApplication minor args arity
+
   visitFalseRec (e : Expr) : M Arg :=
     let arity := 2
     etaIfUnderApplied e arity do
@@ -669,6 +677,8 @@ where
         visitCtor 3 e
       else if declName == ``Eq.casesOn || declName == ``Eq.rec || declName == ``Eq.ndrec then
         visitEqRec e
+      else if declName == ``HEq.casesOn || declName == ``HEq.rec || declName == ``HEq.ndrec then
+        visitHEqRec e
       else if declName == ``And.rec || declName == ``Iff.rec then
         visitAndIffRecCore e (minorPos := 3)
       else if declName == ``And.casesOn || declName == ``Iff.casesOn then