chore: adapt core to preceding syntax change

This commit is contained in:
Sebastian Ullrich 2025-07-16 13:14:47 +02:00 committed by leanprover-bot
parent 1959e6088b
commit 2ed4f39ffe
5 changed files with 5 additions and 5 deletions

View file

@ -12,7 +12,7 @@ public import all Std.Data.DHashMap.Internal.Defs
public import Std.Data.DHashMap.Internal.HashesTo
public import Std.Data.DHashMap.Internal.AssocList.Lemmas
public @[expose] section
@[expose] public section
/-!
This is an internal implementation file of the hash map. Users of the hash map should not rely on

View file

@ -12,7 +12,7 @@ public import Init.Data.Int.DivMod.Basic
public import Init.Data.Int.Linear
public import Init.Data.Nat.Gcd
public @[expose] section
@[expose] public section
namespace Std
namespace Internal

View file

@ -10,7 +10,7 @@ public import Init.Omega
public import Init.Data.Int.DivMod.Lemmas
public import Std.Classes.Ord.Basic
public @[expose] section
@[expose] public section
namespace Std
namespace Time

View file

@ -9,7 +9,7 @@ prelude
public import Std.Classes.Ord.Basic
public import Std.Internal.Rat
public @[expose] section
@[expose] public section
namespace Std
namespace Time

View file

@ -9,7 +9,7 @@ prelude
public import Std.Internal.Rat
public import Std.Time.Time.Unit.Nanosecond
public @[expose] section
@[expose] public section
namespace Std
namespace Time