Spec index operator []

Syntax

spec_index_expr ::= spec_expr [ spec_expr ]

Desugaring

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

Verus/Rust difference

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