macro requires ensures

cryspen · Feb 9, 2025 · e49ac46 · e49ac46
1 parent 98ed62a
commit e49ac46
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/hax-lib/src/dummy.rs b/hax-lib/src/dummy.rs
@@ -39,7 +39,7 @@ pub fn inline_unsafe<T>(_: &str) -> T {
 }
 
 #[doc(hidden)]
-pub fn _internal_loop_invariant<T, P: FnOnce(T) -> bool>(_: P) {}
+pub fn _internal_loop_invariant<T, P: FnOnce(T) -> Prop>(_: P) {}
 
 pub trait Refinement {
     type InnerType;

diff --git a/hax-lib/src/implementation.rs b/hax-lib/src/implementation.rs
@@ -113,7 +113,7 @@ pub fn inline_unsafe<T>(_: &str) -> T {
 
 /// A dummy function that holds a loop invariant.
 #[doc(hidden)]
-pub fn _internal_loop_invariant<T, U:Into<Prop>, P: FnOnce(T) -> U>(_: P) {}
+pub fn _internal_loop_invariant<T, P: FnOnce(T) -> Prop>(_: P) {}
 
 /// A type that implements `Refinement` should be a newtype for a
 /// type `T`. The field holding the value of type `T` should be