From 7316d0b1ece65755d2cfd18e88256db897d864b0 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 19 Aug 2024 10:37:46 +0200 Subject: [PATCH] Fix an issue with the Primitives.fst file --- backends/fstar/Primitives.fst | 2 +- tests/fstar/arrays/Primitives.fst | 2 +- tests/fstar/betree/Primitives.fst | 2 +- tests/fstar/demo/Primitives.fst | 2 +- tests/fstar/hashmap/Primitives.fst | 2 +- tests/fstar/misc/Primitives.fst | 2 +- tests/fstar/rename_attribute/Primitives.fst | 2 +- tests/fstar/traits/Primitives.fst | 2 +- 8 files changed, 8 insertions(+), 8 deletions(-) diff --git a/backends/fstar/Primitives.fst b/backends/fstar/Primitives.fst index 1c7243517..9fa65d9b5 100644 --- a/backends/fstar/Primitives.fst +++ b/backends/fstar/Primitives.fst @@ -267,7 +267,7 @@ let scalar_shr (#ty0 #ty1 : scalar_ty) (x : scalar ty0) (y : scalar ty1) : result (scalar ty0) = admit() -let scalar_not #ty (x : scalar ty) : scalar_ty = admit() +let scalar_not #ty (x : scalar ty) : scalar ty = admit() (** Cast an integer from a [src_ty] to a [tgt_ty] *) // TODO: check the semantics of casts in Rust diff --git a/tests/fstar/arrays/Primitives.fst b/tests/fstar/arrays/Primitives.fst index 1c7243517..9fa65d9b5 100644 --- a/tests/fstar/arrays/Primitives.fst +++ b/tests/fstar/arrays/Primitives.fst @@ -267,7 +267,7 @@ let scalar_shr (#ty0 #ty1 : scalar_ty) (x : scalar ty0) (y : scalar ty1) : result (scalar ty0) = admit() -let scalar_not #ty (x : scalar ty) : scalar_ty = admit() +let scalar_not #ty (x : scalar ty) : scalar ty = admit() (** Cast an integer from a [src_ty] to a [tgt_ty] *) // TODO: check the semantics of casts in Rust diff --git a/tests/fstar/betree/Primitives.fst b/tests/fstar/betree/Primitives.fst index 1c7243517..9fa65d9b5 100644 --- a/tests/fstar/betree/Primitives.fst +++ b/tests/fstar/betree/Primitives.fst @@ -267,7 +267,7 @@ let scalar_shr (#ty0 #ty1 : scalar_ty) (x : scalar ty0) (y : scalar ty1) : result (scalar ty0) = admit() -let scalar_not #ty (x : scalar ty) : scalar_ty = admit() +let scalar_not #ty (x : scalar ty) : scalar ty = admit() (** Cast an integer from a [src_ty] to a [tgt_ty] *) // TODO: check the semantics of casts in Rust diff --git a/tests/fstar/demo/Primitives.fst b/tests/fstar/demo/Primitives.fst index 1c7243517..9fa65d9b5 100644 --- a/tests/fstar/demo/Primitives.fst +++ b/tests/fstar/demo/Primitives.fst @@ -267,7 +267,7 @@ let scalar_shr (#ty0 #ty1 : scalar_ty) (x : scalar ty0) (y : scalar ty1) : result (scalar ty0) = admit() -let scalar_not #ty (x : scalar ty) : scalar_ty = admit() +let scalar_not #ty (x : scalar ty) : scalar ty = admit() (** Cast an integer from a [src_ty] to a [tgt_ty] *) // TODO: check the semantics of casts in Rust diff --git a/tests/fstar/hashmap/Primitives.fst b/tests/fstar/hashmap/Primitives.fst index 1c7243517..9fa65d9b5 100644 --- a/tests/fstar/hashmap/Primitives.fst +++ b/tests/fstar/hashmap/Primitives.fst @@ -267,7 +267,7 @@ let scalar_shr (#ty0 #ty1 : scalar_ty) (x : scalar ty0) (y : scalar ty1) : result (scalar ty0) = admit() -let scalar_not #ty (x : scalar ty) : scalar_ty = admit() +let scalar_not #ty (x : scalar ty) : scalar ty = admit() (** Cast an integer from a [src_ty] to a [tgt_ty] *) // TODO: check the semantics of casts in Rust diff --git a/tests/fstar/misc/Primitives.fst b/tests/fstar/misc/Primitives.fst index 1c7243517..9fa65d9b5 100644 --- a/tests/fstar/misc/Primitives.fst +++ b/tests/fstar/misc/Primitives.fst @@ -267,7 +267,7 @@ let scalar_shr (#ty0 #ty1 : scalar_ty) (x : scalar ty0) (y : scalar ty1) : result (scalar ty0) = admit() -let scalar_not #ty (x : scalar ty) : scalar_ty = admit() +let scalar_not #ty (x : scalar ty) : scalar ty = admit() (** Cast an integer from a [src_ty] to a [tgt_ty] *) // TODO: check the semantics of casts in Rust diff --git a/tests/fstar/rename_attribute/Primitives.fst b/tests/fstar/rename_attribute/Primitives.fst index 1c7243517..9fa65d9b5 100644 --- a/tests/fstar/rename_attribute/Primitives.fst +++ b/tests/fstar/rename_attribute/Primitives.fst @@ -267,7 +267,7 @@ let scalar_shr (#ty0 #ty1 : scalar_ty) (x : scalar ty0) (y : scalar ty1) : result (scalar ty0) = admit() -let scalar_not #ty (x : scalar ty) : scalar_ty = admit() +let scalar_not #ty (x : scalar ty) : scalar ty = admit() (** Cast an integer from a [src_ty] to a [tgt_ty] *) // TODO: check the semantics of casts in Rust diff --git a/tests/fstar/traits/Primitives.fst b/tests/fstar/traits/Primitives.fst index 1c7243517..9fa65d9b5 100644 --- a/tests/fstar/traits/Primitives.fst +++ b/tests/fstar/traits/Primitives.fst @@ -267,7 +267,7 @@ let scalar_shr (#ty0 #ty1 : scalar_ty) (x : scalar ty0) (y : scalar ty1) : result (scalar ty0) = admit() -let scalar_not #ty (x : scalar ty) : scalar_ty = admit() +let scalar_not #ty (x : scalar ty) : scalar ty = admit() (** Cast an integer from a [src_ty] to a [tgt_ty] *) // TODO: check the semantics of casts in Rust