diff options
Diffstat (limited to 'src/Wasm/Expression/Utilities.agda')
| -rw-r--r-- | src/Wasm/Expression/Utilities.agda | 21 |
1 files changed, 11 insertions, 10 deletions
diff --git a/src/Wasm/Expression/Utilities.agda b/src/Wasm/Expression/Utilities.agda index b7f9af4..129af14 100644 --- a/src/Wasm/Expression/Utilities.agda +++ b/src/Wasm/Expression/Utilities.agda @@ -5,9 +5,10 @@ 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) +Vec′ A = Vec≤ A 2^32 data Signedness : Set where Signed : Signedness @@ -24,28 +25,28 @@ module BitWidth′ where module Indices where TypeIdx : Set - TypeIdx = Fin (2 ^ 32) + TypeIdx = Fin 2^32 FuncIdx : Set - FuncIdx = Fin (2 ^ 32) + FuncIdx = Fin 2^32 TableIdx : Set - TableIdx = Fin (2 ^ 32) + TableIdx = Fin 2^32 MemIdx : Set - MemIdx = Fin (2 ^ 32) + MemIdx = Fin 2^32 GlobalIdx : Set - GlobalIdx = Fin (2 ^ 32) + GlobalIdx = Fin 2^32 ElemIdx : Set - ElemIdx = Fin (2 ^ 32) + ElemIdx = Fin 2^32 DataIdx : Set - DataIdx = Fin (2 ^ 32) + DataIdx = Fin 2^32 LocalIdx : Set - LocalIdx = Fin (2 ^ 32) + LocalIdx = Fin 2^32 LabelIdx : Set - LabelIdx = Fin (2 ^ 32) + LabelIdx = Fin 2^32 |