diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2021-08-10 19:11:38 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2021-08-10 19:11:38 +0100 |
| commit | 904924c33720c3481f738966f32e9c34736f92cf (patch) | |
| tree | 0365bccd7afa6a0c4031866e8681f495a1e3c8bf /src/Wasm/Value.agda | |
| parent | a3a8a44b4bc0d60164452826645066a5ffed5bc5 (diff) | |
Rewrite so only valid modules can be constructed.
Diffstat (limited to 'src/Wasm/Value.agda')
| -rw-r--r-- | src/Wasm/Value.agda | 24 |
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 |