From 904924c33720c3481f738966f32e9c34736f92cf Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Tue, 10 Aug 2021 19:11:38 +0100
Subject: Rewrite so only valid modules can be constructed.

---
 src/Wasm/Expression/Utilities.agda | 52 --------------------------------------
 1 file changed, 52 deletions(-)
 delete mode 100644 src/Wasm/Expression/Utilities.agda

(limited to 'src/Wasm/Expression/Utilities.agda')

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
-- 
cgit v1.2.3