summaryrefslogtreecommitdiff
path: root/src/Wasm/Expression/Utilities.agda
diff options
context:
space:
mode:
Diffstat (limited to 'src/Wasm/Expression/Utilities.agda')
-rw-r--r--src/Wasm/Expression/Utilities.agda52
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