aboutsummaryrefslogtreecommitdiff
path: root/kernel/prelude/SATS/safe_casts.sats
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/prelude/SATS/safe_casts.sats')
-rw-r--r--kernel/prelude/SATS/safe_casts.sats1
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/prelude/SATS/safe_casts.sats b/kernel/prelude/SATS/safe_casts.sats
new file mode 100644
index 0000000..50a68a8
--- /dev/null
+++ b/kernel/prelude/SATS/safe_casts.sats
@@ -0,0 +1 @@
+castfn u2uint64{v : nat | v <= 0xFFFFFFFFFFFFFFFF}(v : uint v) : uint64 v