blob: 2cb07a5d4cec27a58c56eea79a536b5a25dfa742 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
|
Require Export ConstrainedComputation.
Notation "const A" := CConst A.
Notation "var A" := CVar A.
Notation "A : B" := CJoin A B.
Notation "left A" := CLeft A.
Notation "right A" := CRight A.
Notation "~ A" := UnaryExpr CNot A.
Notation "- A" := UnaryExpr COpp A.
Notation "A + B" := BinaryExpr CPlus A B.
Notation "A - B" := BinaryExpr CMinus A B.
Notation "A * B" := BinaryExpr CMult A B.
Notation "A / B" := BinaryExpr CDiv A B.
Notation "A & B" := BinaryExpr CAnd A B.
Notation "A | B" := BinaryExpr COr A B.
Notation "A ^ B" := BinaryExpr CXor A B.
Notation "A >> B" := BinaryExpr CRShift A B.
Notation "A << B" := BinaryExpr CLShift A B.
Definition toExpr {type} (term: CTerm type) = TermExpr term.
Coersion toExpr: {type} CTerm type >-> CExpr type.
Notation "ret A" := CRet A
Notation "A . B" := CCompose A B
Notation "A ? B : C" := CIte A B C
Notation "set A to B in C" := CLet A B C
|
