From 9812bb2ae394b59ae9fcb7cf9b78fd260aa3e92a Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Wed, 28 Jul 2021 16:55:28 +0100 Subject: Cleanup before working on 'Modules' --- src/Wasm/Expression/Values.agda | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'src/Wasm/Expression/Values.agda') diff --git a/src/Wasm/Expression/Values.agda b/src/Wasm/Expression/Values.agda index d6bce60..283e325 100644 --- a/src/Wasm/Expression/Values.agda +++ b/src/Wasm/Expression/Values.agda @@ -9,6 +9,7 @@ open import Data.Char using (Char; toℕ) open import Data.Empty using (⊥) open import Data.Fin using (Fin) open import Data.Nat using (ℕ; zero; suc; _^_; pred) +open import Wasm.Constants open import Wasm.Expression.Utilities using (BitWidth; 32Bit; 64Bit) infix 8 +_ -_ @@ -115,4 +116,7 @@ module _ where byteLength s = sum (map utf8Bytes (toList s)) data Name : Set where - name : ∀ s → {len : byteLength s < 2 ^ 32} → Name + name : ∀ s → {len : byteLength s < 2^32} → Name + + toString : Name → String + toString (name s) = s -- cgit v1.2.3