diff options
Diffstat (limited to 'src/Wasm/Expression/Values.agda')
| -rw-r--r-- | src/Wasm/Expression/Values.agda | 6 |
1 files changed, 5 insertions, 1 deletions
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 |