Merge pull request #1352 from cryspen/prop-eq-any-type

hax-lib: prop: allow equality on every type

Author: W95Psp

hax-lib/src/prop.rs

@@ -21,18 +21,24 @@ pub mod constructors {
     pub fn not(lhs: Prop) -> Prop {
         Prop(!lhs.0)
     }
-    pub fn eq(lhs: Prop, other: Prop) -> Prop {
-        Prop(lhs.0 == other.0)
+
+    /// Logical equality between two value of *any* type
+    pub fn eq<T>(_lhs: T, _rhs: T) -> Prop {
+        Prop(true)
     }
-    pub fn ne(lhs: Prop, other: Prop) -> Prop {
-        Prop(lhs.0 != other.0)
+
+    pub fn ne<T>(_lhs: T, _rhs: T) -> Prop {
+        Prop(true)
     }
+
     pub fn implies(lhs: Prop, other: Prop) -> Prop {
         Prop(lhs.0 || !other.0)
     }
+
     pub fn forall<A, F: Fn(A) -> Prop>(_pred: F) -> Prop {
         Prop(true)
     }
+
     pub fn exists<A, F: Fn(A) -> Prop>(_pred: F) -> Prop {
         Prop(true)
     }
@@ -136,3 +142,5 @@ pub fn exists<T, U: Into<Prop>>(f: impl Fn(T) -> U) -> Prop {
 pub fn implies(lhs: impl Into<Prop>, rhs: impl Into<Prop>) -> Prop {
     constructors::implies(lhs.into(), rhs.into())
 }
+
+pub use constructors::eq;