Fix imports

jonsterling · Oct 5, 2023 · 50ac0bb · 50ac0bb
1 parent c3819d0
commit 50ac0bb
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git a/src/Calf/Data/IsBounded.agda b/src/Calf/Data/IsBounded.agda
@@ -13,7 +13,7 @@ open import Calf.CBPV
 open import Calf.Directed
 open import Calf.Step costMonoid
 
-open import Calf.Data.IsBoundedG costMonoid public
+open import Calf.Data.IsBoundedG costMonoid
 
 
 IsBounded : (A : tp⁺) → cmp (F A) → ℂ → Set

diff --git a/src/Examples/Decalf/HigherOrderFunction.agda b/src/Examples/Decalf/HigherOrderFunction.agda
@@ -15,6 +15,7 @@ open import Calf.Data.List using (list; []; _∷_; [_]; _++_; length)
 open import Calf.Data.Bool using (bool; if_then_else_)
 open import Calf.Data.Product using (unit)
 open import Calf.Data.Equality as Eq using (_≡_; refl; module ≡-Reasoning)
+open import Calf.Data.IsBoundedG costMonoid using (step⋆)
 open import Calf.Data.IsBounded costMonoid
 open import Function