These are right-hand-side expressions of the MiniC language, i.e., expressions that may occur on the right-hand side of an assignment.

• RhsVar(vn) is a variable with name vn.
• ConstB(b) is the Cbool value b as a machine word.
• ConstN(i) is the Cnat value i as a machine word.
• ConstZ(i) is the Cint value i as a machine word.
• Apply1(op1,e) is the application of the unary operator op1 to the MiniC expression e.
• Apply2(op2,e1,e2) is the application of the binary operator op2 to the MiniC expressions e1 and e2.
• CndExpr(e0,e1,e2) is a conditional expression that evaluates to e1 if e0 evaluates to true and otherwise it evaluates to e2.
• FunApp(f,[|e1,...,en|]) is the application of function f to the argument expressions e1,...,en.
• RhsArrAcc(lhs,e) refers to array element lhs[e].
• RhsTupAcc(lhs,i) refers to tuple element lhs.i.
• ArrNew [|e1,...,en|] constructs an array.
• TupNew [|e1,...,en|] constructs a tuple.