From b280a889f7342ca71ca537722309c2353a36f63c Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Thu, 26 Feb 2026 18:30:11 +0100
Subject: [PATCH] parser: fail upon duplicate declarations

While most attacks involving duplicate declarations that actually prove
False would still be caught if one delaration is simply ignored, it
seems safer to catch this early and for all users of the parser. At
least until someone comes up with a use case for duplicate declarations
in the same file.
---
 Export/Parse.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/Export/Parse.lean b/Export/Parse.lean
index 820c02b..1eedbab 100644
--- a/Export/Parse.lean
+++ b/Export/Parse.lean
@@ -76,6 +76,8 @@ def addRecursorRule (ridx : Nat) (r : Lean.RecursorRule) : M Unit := do
 
 @[inline]
 def addConst (name : Lean.Name) (d : Lean.ConstantInfo) : M Unit := do
+  if (← get).constMap.contains name then
+    fail s!"Duplicate declaration: {name}"
   modify fun s => {
     s with
       constMap := s.constMap.insert name d