vstd
In vstd::relations
?
Settings
Function
vstd
::
relations
::
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) }