vstd
In vstd::
relations
vstd
::
relations
Function
reflexive
Copy item path
Source
pub
open spec
fn reflexive<T>(r:
FnSpec
<
(T, T)
,
bool
>) ->
bool
Expand description
{ forall |x: T|
#[trigger]
r(x, x) }