From e9f1c38b6322b417ec95be978c01f29270caa227 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Sat, 20 Dec 2025 00:00:33 +0000
Subject: [PATCH 1/4] Initial plan


From 24358dbc0e810a4c8b04d0d56438dc3bc2dbcc59 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Sat, 20 Dec 2025 00:12:23 +0000
Subject: [PATCH 2/4] Fix: Handle all ConstantInfo types and improve error
 message

- Add support for def, opaque, quot, inductive, constructor, and recursor constants
- Add constantKindName helper to show actual types in error messages
- Error message now shows what kinds were found when they don't match

Co-authored-by: JasonGross <396076+JasonGross@users.noreply.github.com>
---
 Comparator/Compare.lean | 20 +++++++++++++++++++-
 1 file changed, 19 insertions(+), 1 deletion(-)

diff --git a/Comparator/Compare.lean b/Comparator/Compare.lean
index 1e0aff5..9390ecb 100644
--- a/Comparator/Compare.lean
+++ b/Comparator/Compare.lean
@@ -54,6 +54,18 @@ partial def loop : CompareM Unit := do
 
 end Compare
 
+/-- Get a human-readable name for the kind of constant -/
+def constantKindName (info : Lean.ConstantInfo) : String :=
+  match info with
+  | .axiomInfo .. => "axiom"
+  | .defnInfo .. => "def"
+  | .thmInfo .. => "theorem"
+  | .opaqueInfo .. => "opaque"
+  | .quotInfo .. => "quot"
+  | .inductInfo .. => "inductive"
+  | .ctorInfo .. => "constructor"
+  | .recInfo .. => "recursor"
+
 def compareAt (challenge solution : ExportedEnv) (targets : Array Lean.Name) :
     Except String Unit := do
   let mut worklist := #[]
@@ -69,7 +81,13 @@ def compareAt (challenge solution : ExportedEnv) (targets : Array Lean.Name) :
       match challengeConst, solutionConst with
       | .thmInfo cc, .thmInfo sc
       | .axiomInfo cc, .axiomInfo sc => pure (cc.toConstantVal, sc.toConstantVal)
-      | _, _ => throw s!"Challenge and solution constant kind don't match: '{target}'"
+      | .defnInfo cc, .defnInfo sc
+      | .opaqueInfo cc, .opaqueInfo sc => pure (cc.toConstantVal, sc.toConstantVal)
+      | .quotInfo cc, .quotInfo sc => pure (cc.toConstantVal, sc.toConstantVal)
+      | .inductInfo cc, .inductInfo sc => pure (cc.toConstantVal, sc.toConstantVal)
+      | .ctorInfo cc, .ctorInfo sc => pure (cc.toConstantVal, sc.toConstantVal)
+      | .recInfo cc, .recInfo sc => pure (cc.toConstantVal, sc.toConstantVal)
+      | c, s => throw s!"Challenge and solution constant kind don't match: '{target}' (challenge: {constantKindName c}, solution: {constantKindName s})"
 
     if challengeConst != solutionConst then
       throw s!"Challenge and solution theorem statement do not match: '{target}'"

From a7743e709d2d2b2fe01bfecbff88448ba5a07a73 Mon Sep 17 00:00:00 2001
From: Jason Gross <jasongross9@gmail.com>
Date: Fri, 19 Dec 2025 16:39:41 -0800
Subject: [PATCH 3/4] Update Comparator/Compare.lean

---
 Comparator/Compare.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Comparator/Compare.lean b/Comparator/Compare.lean
index 9390ecb..29bd5e0 100644
--- a/Comparator/Compare.lean
+++ b/Comparator/Compare.lean
@@ -82,10 +82,10 @@ def compareAt (challenge solution : ExportedEnv) (targets : Array Lean.Name) :
       | .thmInfo cc, .thmInfo sc
       | .axiomInfo cc, .axiomInfo sc => pure (cc.toConstantVal, sc.toConstantVal)
       | .defnInfo cc, .defnInfo sc
-      | .opaqueInfo cc, .opaqueInfo sc => pure (cc.toConstantVal, sc.toConstantVal)
-      | .quotInfo cc, .quotInfo sc => pure (cc.toConstantVal, sc.toConstantVal)
-      | .inductInfo cc, .inductInfo sc => pure (cc.toConstantVal, sc.toConstantVal)
-      | .ctorInfo cc, .ctorInfo sc => pure (cc.toConstantVal, sc.toConstantVal)
+      | .opaqueInfo cc, .opaqueInfo sc
+      | .quotInfo cc, .quotInfo sc
+      | .inductInfo cc, .inductInfo sc
+      | .ctorInfo cc, .ctorInfo sc
       | .recInfo cc, .recInfo sc => pure (cc.toConstantVal, sc.toConstantVal)
       | c, s => throw s!"Challenge and solution constant kind don't match: '{target}' (challenge: {constantKindName c}, solution: {constantKindName s})"
 

From 9d18645681f9a6907846d482cded8fd18b8412ba Mon Sep 17 00:00:00 2001
From: Jason Gross <jasongross9@gmail.com>
Date: Fri, 19 Dec 2025 17:11:56 -0800
Subject: [PATCH 4/4] Update Comparator/Compare.lean

---
 Comparator/Compare.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Comparator/Compare.lean b/Comparator/Compare.lean
index 29bd5e0..d55379c 100644
--- a/Comparator/Compare.lean
+++ b/Comparator/Compare.lean
@@ -80,7 +80,7 @@ def compareAt (challenge solution : ExportedEnv) (targets : Array Lean.Name) :
     let (challengeConst, solutionConst) ←
       match challengeConst, solutionConst with
       | .thmInfo cc, .thmInfo sc
-      | .axiomInfo cc, .axiomInfo sc => pure (cc.toConstantVal, sc.toConstantVal)
+      | .axiomInfo cc, .axiomInfo sc
       | .defnInfo cc, .defnInfo sc
       | .opaqueInfo cc, .opaqueInfo sc
       | .quotInfo cc, .quotInfo sc