lib extensions

cryspen · Feb 2, 2025 · 59ff7cd · 59ff7cd
1 parent 3d2cbc0
commit 59ff7cd
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 1 deletion.
diff --git a/proof-libs/fstar/core/Core.Array.fsti b/proof-libs/fstar/core/Core.Array.fsti
@@ -8,6 +8,6 @@ let impl_23__map #a n #b (arr: t_Array a n) (f: a -> b): t_Array b n
 
 let impl_23__as_slice #a len (arr: t_Array a len): t_Slice a = arr
 
-val from_fn #a len (f: usize -> a): Pure (t_Array a len) (requires True) (ensures (fun a -> forall i. Seq.index a i == f (sz i)))
+val from_fn #a len (f: (x:usize{x <. len}) -> a): Pure (t_Array a len) (requires True) (ensures (fun a -> forall i. Seq.index a i == f (sz i)))
 
 
diff --git a/proof-libs/fstar/core/Core.Num.fsti b/proof-libs/fstar/core/Core.Num.fsti
@@ -2,6 +2,8 @@ module Core.Num
 open Rust_primitives
 
 let impl_u16__MAX: u16 = mk_u16 (maxint u16_inttype)
+let impl_i32__MAX: i32 = mk_i32 (maxint i32_inttype)
+let impl_i32__MIN: i32 = mk_i32 (minint i32_inttype)
 
 let impl_u8__wrapping_add: u8 -> u8 -> u8 = add_mod
 let impl_u8__wrapping_sub: u8 -> u8 -> u8 = sub_mod
Original file line number	Diff line number	Diff line change
Expand Up		@@ -8,6 +8,6 @@ let impl_23__map #a n #b (arr: t_Array a n) (f: a -> b): t_Array b n

		let impl_23__as_slice #a len (arr: t_Array a len): t_Slice a = arr

		val from_fn #a len (f: usize -> a): Pure (t_Array a len) (requires True) (ensures (fun a -> forall i. Seq.index a i == f (sz i)))
		val from_fn #a len (f: (x:usize{x <. len}) -> a): Pure (t_Array a len) (requires True) (ensures (fun a -> forall i. Seq.index a i == f (sz i)))