Spec expressions

Here we discuss the syntax and semantics for pure specification expressions.

Syntax

spec_expr ::= fn_call_expr
            | and_expr
            | or_expr
            | not_expr
            | if_expr
            | if_let_expr
            | match_expr
            | spec_block_expr
            | as_expr
            | box_new_expr
            | ref_expr
            | deref_expr
            | chained_expr
            | implies_expr
            | explies_expr
            | iff_expr
            | arith_expr
            | ineq_expr
            | bit_expr
            | equality_expr
            | ext_eq_expr
            | prefix_and_expr
            | prefix_or_expr
            | forall_expr
            | exists_expr
            | choose_expr
            | root_trigger_attr_expr
            | inner_trigger_attr_expr
            | view_expr
            | spec_index_expr
            | has_expr
            | is_expr
            | matches_expr
            | decreases_to_expr
            | ( spec_expr )