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