diff options
| author |  Robert Sloan <varomodt@gmail.com> | 2016-06-02 21:50:39 -0400 |
|---|---|---|
| committer | Robert Sloan <varomodt@gmail.com> | 2016-06-22 13:43:38 -0400 |
| commit | f5ea287ab5f79dc7edf2b1ad85b145d370c03ed0 (patch) | |
| tree | bf5a9fa0cc842bfb30acc7641b324dba58b46c76 /src/Assembly/Pseudo.v | |
| parent | d3c45ab10d26905572c90ee621344b4357a54d7a (diff) | |
Running PipelineExample
Diffstat (limited to 'src/Assembly/Pseudo.v')
| -rw-r--r-- | src/Assembly/Pseudo.v | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/src/Assembly/Pseudo.v b/src/Assembly/Pseudo.v index 21cc11c4e..ce2c5878a 100644 --- a/src/Assembly/Pseudo.v +++ b/src/Assembly/Pseudo.v @@ -106,6 +106,13 @@ Module Pseudo (M: PseudoMachine) <: Language. Definition evaluatesTo := fun (p: Program) (st st': State) => (pseudoEval p st = Some st'). + Module Notations. + Delimit Scope pseudo_notations with p. + Open Scope pseudo_notations. + + Notation "'LET' A := B 'IN' C" (at level 60, right associativity) : pseudo_notations. + End Notations. + (* world peace *) End Pseudo. @@ -121,5 +128,4 @@ Module PseudoUnary64 <: PseudoMachine. Definition vars := 1. Definition width_spec := W64. Definition const: Type := word width. -End PseudoUnary64. -
\ No newline at end of file +End PseudoUnary64.
\ No newline at end of file |