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
index 8850ef6..f93a2be 100644
--- a/kernel/prelude/SATS/safe_casts.sats
+++ b/kernel/prelude/SATS/safe_casts.sats
@@ -10,3 +10,4 @@ castfn ulint_to_Ptr0(v : ulint):<> Ptr0
castfn sz_to_Ptr0(v : size_t):<> Ptr0
castfn Ptr1_to_sz(v : Ptr1):<> sizeGte(1)
+castfn Ptr0_to_sz(v : Ptr0):<> size_t