diff options
Diffstat (limited to 'src/Assembly/Pipeline.v')
| -rw-r--r-- | src/Assembly/Pipeline.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Assembly/Pipeline.v b/src/Assembly/Pipeline.v index 97aa94d36..8e58e7345 100644 --- a/src/Assembly/Pipeline.v +++ b/src/Assembly/Pipeline.v @@ -27,6 +27,7 @@ Module PipelineExamples. Local Notation "v [[ i ]]" := (nth i v (wzero _)) (at level 40). Local Notation "$$ v" := (natToWord _ v) (at level 40). + (* Definition add_example: @pseudeq 32 W32 1 1 (fun v => plet a := $$ 1 in plet b := v[[0]] in @@ -63,7 +64,6 @@ Module PipelineExamples. Definition mult_ex_str := (Pipeline.toString (proj1_sig mult_example)). - (* Definition comb_example: @pseudeq 32 W32 1 1 (fun v => plet a := $$ 7 in plet b := v[[0]] in |