diff --git a/src/Init/Data/Dyadic/Instances.lean b/src/Init/Data/Dyadic/Instances.lean index c7fcea5827..363658375b 100644 --- a/src/Init/Data/Dyadic/Instances.lean +++ b/src/Init/Data/Dyadic/Instances.lean @@ -11,6 +11,8 @@ public import Init.Grind.Ordered.Ring /-! # Internal `grind` algebra instances for `Dyadic`. -/ +@[expose] public section + open Lean.Grind namespace Dyadic diff --git a/src/Init/Data/Dyadic/Inv.lean b/src/Init/Data/Dyadic/Inv.lean index 1f66fdffc3..356f2fee72 100644 --- a/src/Init/Data/Dyadic/Inv.lean +++ b/src/Init/Data/Dyadic/Inv.lean @@ -4,7 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ module + prelude +public import Init.Data.Dyadic.Basic import Init.Data.Dyadic.Round import Init.Grind.Ordered.Ring @@ -12,6 +14,8 @@ import Init.Grind.Ordered.Ring # Inversion for dyadic numbers -/ +@[expose] public section + namespace Dyadic /-- diff --git a/src/Init/Data/Dyadic/Round.lean b/src/Init/Data/Dyadic/Round.lean index 13ff921616..aaab5f1a2a 100644 --- a/src/Init/Data/Dyadic/Round.lean +++ b/src/Init/Data/Dyadic/Round.lean @@ -7,7 +7,7 @@ module prelude public import Init.Data.Dyadic.Basic -import all Init.Data.Dyadic.Instances +import Init.Data.Dyadic.Instances import Init.Grind.Ordered.Rat import Init.Grind.Ordered.Field