diff options
Diffstat (limited to 'src/Assembly/DSL.v')
| -rw-r--r-- | src/Assembly/DSL.v | 28 |
1 files changed, 0 insertions, 28 deletions
diff --git a/src/Assembly/DSL.v b/src/Assembly/DSL.v deleted file mode 100644 index 2cb07a5d4..000000000 --- a/src/Assembly/DSL.v +++ /dev/null @@ -1,28 +0,0 @@ - -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 |