The view function @ #

Syntax #

V@[view_expr] ::= V@[spec_expr] @

Desugaring #

The expression expr@ desugars to the expression expr.view(), which is resolved as normal via Rust's method resolution. This usually, but not always, resolves to the view method defined by the View trait.

Examples #

By convention, the view() function is a spec function for the abstraction of an exec-mode object. See, for example:

• Using view to reason about Vec
• Defining a view function