Fix an issue with the Primitives.fst file

AeneasVerif · Aug 19, 2024 · 7316d0b · 7316d0b
1 parent f7dc78f
commit 7316d0b
Show file tree

Hide file tree

Showing 8 changed files with 8 additions and 8 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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