From d4f9232345c1f9bb8ac96dab00b02af01e5c420b Mon Sep 17 00:00:00 2001
From: Alexander Bentkamp <alexander@cryspen.com>
Date: Thu, 11 Jun 2026 11:49:01 +0200
Subject: [PATCH] fix: comment out dummy Slice definition

---
 lean/CoreModels/Core/Types.lean | 2 ++
 patch_lean.py                   | 1 +
 2 files changed, 3 insertions(+)

diff --git a/lean/CoreModels/Core/Types.lean b/lean/CoreModels/Core/Types.lean
index 3740284..0b8cce0 100644
--- a/lean/CoreModels/Core/Types.lean
+++ b/lean/CoreModels/Core/Types.lean
@@ -795,10 +795,12 @@ structure ops.range.RangeInclusive (T : Type) where
   start : T
   «end» : T
 
+/-
 /-- [core_models::slice::Slice]
     Source: 'core-models/src/core/slice.rs', lines 5:0-5:19 -/
 @[reducible]
 def slice.Slice (T : Type) := T
+-/
 
 /-- [core_models::slice::iter::Chunks]
     Source: 'core-models/src/core/slice.rs', lines 12:4-15:5
diff --git a/patch_lean.py b/patch_lean.py
index d7fe1fd..c5c31bc 100755
--- a/patch_lean.py
+++ b/patch_lean.py
@@ -263,6 +263,7 @@ def comment_out_types(text: str) -> str:
         "core_models::cmp::Ordering",
         "core_models::option::Option",
         "core_models::result::Result",
+        "core_models::slice::Slice",
     ])
 
 def add_funs_prologue_import(text: str) -> str: