summaryrefslogtreecommitdiff
path: root/src/Wasm/Value.agda
diff options
context:
space:
mode:
Diffstat (limited to 'src/Wasm/Value.agda')
-rw-r--r--src/Wasm/Value.agda24
1 files changed, 24 insertions, 0 deletions
diff --git a/src/Wasm/Value.agda b/src/Wasm/Value.agda
new file mode 100644
index 0000000..9dfc24e
--- /dev/null
+++ b/src/Wasm/Value.agda
@@ -0,0 +1,24 @@
+{-# OPTIONS --safe --without-K #-}
+
+module Wasm.Value where
+
+open import Data.Fin using (Fin)
+open import Data.String using (String)
+
+Name : Set
+Name = String
+
+Byte : Set
+Byte = Fin 256
+
+I32 : Set
+I32 = Fin 4294967296
+
+I64 : Set
+I64 = Fin 18446744073709551616
+
+F32 : Set
+F32 = Fin 4294967296
+
+F64 : Set
+F64 = Fin 18446744073709551616