Rewrite so only valid modules can be constructed.

1 files changed, 0 insertions, 52 deletions

diff --git a/src/Wasm/Expression/Utilities.agda b/src/Wasm/Expression/Utilities.agda
deleted file mode 100644
index 129af14..0000000
--- a/src/Wasm/Expression/Utilities.agda
+++ /dev/null
@@ -1,52 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-module Wasm.Expression.Utilities where
-
-open import Data.Fin using (Fin)
-open import Data.Nat using (ℕ; _^_)
-open import Data.Vec.Bounded using (Vec≤)
-open import Wasm.Constants
-
-Vec′ : ∀ {a} → Set a → Set a
-Vec′ A = Vec≤ A 2^32
-
-data Signedness : Set where
-  Signed   : Signedness
-  Unsigned : Signedness
-
-data BitWidth : Set where
-  32Bit : BitWidth
-  64Bit : BitWidth
-
-module BitWidth′ where
-  toℕ : BitWidth → ℕ
-  toℕ 32Bit = 32
-  toℕ 64Bit = 64
-
-module Indices where
-  TypeIdx : Set
-  TypeIdx = Fin 2^32
-
-  FuncIdx : Set
-  FuncIdx = Fin 2^32
-
-  TableIdx : Set
-  TableIdx = Fin 2^32
-
-  MemIdx : Set
-  MemIdx = Fin 2^32
-
-  GlobalIdx : Set
-  GlobalIdx = Fin 2^32
-
-  ElemIdx : Set
-  ElemIdx = Fin 2^32
-
-  DataIdx : Set
-  DataIdx = Fin 2^32
-
-  LocalIdx : Set
-  LocalIdx = Fin 2^32
-
-  LabelIdx : Set
-  LabelIdx = Fin 2^32