Trait FiniteRange
Source pub trait FiniteRange: Sized {
// Required methods
spec fn range_set(lo: Self, hi: Self) -> Set<Self>;
spec fn range_len(lo: Self, hi: Self) -> nat;
proof fn range_properties(lo: Self, hi: Self);
}
ensuresSelf::range_set(lo, hi).finite(),
Self::range_set(lo, hi).len() == Self::range_len(lo, hi),
This trait is not dyn compatible.
In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.
{ Set::new(|i: Self| lo <= i < hi) }
{ if lo <= hi { (hi - lo) as nat } else { 0 } }
{ Set::new(|i: Self| lo <= i < hi) }
{ if lo <= hi { (hi - lo) as nat } else { 0 } }
{ Set::new(|i: Self| lo <= i < hi) }
{ if lo <= hi { (hi - lo) as nat } else { 0 } }
{ Set::new(|i: Self| lo <= i < hi) }
{ if lo <= hi { (hi - lo) as nat } else { 0 } }
{ Set::new(|i: Self| lo <= i < hi) }
{ if lo <= hi { (hi - lo) as nat } else { 0 } }
{ Set::new(|i: Self| lo <= i < hi) }
{ if lo <= hi { (hi - lo) as nat } else { 0 } }
{ Set::new(|i: Self| lo <= i < hi) }
{ if lo <= hi { (hi - lo) as nat } else { 0 } }
{ Set::new(|i: Self| lo <= i < hi) }
{ if lo <= hi { (hi - lo) as nat } else { 0 } }
{ Set::new(|i: Self| lo <= i < hi) }
{ if lo <= hi { (hi - lo) as nat } else { 0 } }
{ Set::new(|i: Self| lo <= i < hi) }
{ if lo <= hi { (hi - lo) as nat } else { 0 } }
{ Set::new(|i: Self| lo <= i < hi) }
{ if lo <= hi { (hi - lo) as nat } else { 0 } }
{ Set::new(|i: Self| lo <= i < hi) }
{ if lo <= hi { (hi - lo) as nat } else { 0 } }