Function axiom_spec_range_inclusive_new

Source

pub broadcast proof fn axiom_spec_range_inclusive_new<Idx>(start: Idx, end: Idx)

Expand description

ensures

(#[trigger] spec_range_inclusive_new(start, end))@
    == {
        RangeInclusiveView {
            start,
            end,
            exhausted: false,
        }
    },

axiom_spec_range_inclusive_new

Function axiom_spec_range_inclusive_new Copy item path

Function axiom_spec_range_inclusive_new