vstd
In vstd::
relations
Functions
antisymmetric
associative
asymmetric
commutative
connected
equivalence_relation
injective
irreflexive
is_greatest
is_least
is_maximal
is_minimal
lemma_new_first_element_still_sorted_by
partial_ordering
pre_ordering
reflexive
sorted_by
strict_total_ordering
strongly_connected
symmetric
total_ordering
transitive
?
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) }