Spec index operator [] #

Syntax #

V@[spec_index_expr] ::= V@[spec_expr] [ V@[spec_expr] ]

Desugaring #

In spec code, the expression expr[i] desugars to expr.spec_index(i), which is resolved as normal via Rust's method resolution.

[!DIFF] This is different than the index operator in executable code, where it is either a place expression indexing into a slice or an array, or is overloaded via the Index or IndexMut traits.

Use cases #

For example:

• spec_index for a Seq
• spec_index for a Map
• spec_index for a slice