From cfc4fdd913f5c488f81ab0dfbf3887c7883f2dfb Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 22 Feb 2024 18:32:30 +0100 Subject: [PATCH] More import pruning --- src/Init/Data/String/Extra.lean | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/Init/Data/String/Extra.lean b/src/Init/Data/String/Extra.lean index a5f1912fb416..c07abb6cdeaf 100644 --- a/src/Init/Data/String/Extra.lean +++ b/src/Init/Data/String/Extra.lean @@ -4,11 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura -/ prelude -import Init.Control.Except import Init.Data.ByteArray -import Init.SimpLemmas -import Init.Util -import Init.WFTactics namespace String