diff options
| author |  Robert Sloan <varomodt@gmail.com> | 2016-06-23 00:21:52 -0400 |
|---|---|---|
| committer | Robert Sloan <varomodt@gmail.com> | 2016-06-23 00:21:52 -0400 |
| commit | 6ea5d70f608ec5b3aea485843e677ce84ace6648 (patch) | |
| tree | 4ac7f5a188ea2a7ee01f600fb21c48489c3be84b /src/Assembly | |
| parent | 4c727f5bf4830b2d41c7528f6a825c7d0a4ea295 (diff) | |
Pseudize Let_In with minor notations
Diffstat (limited to 'src/Assembly')
| -rw-r--r-- | src/Assembly/Pseudize.v | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/src/Assembly/Pseudize.v b/src/Assembly/Pseudize.v index 915e28212..5b4c9c5b6 100644 --- a/src/Assembly/Pseudize.v +++ b/src/Assembly/Pseudize.v @@ -256,10 +256,14 @@ Module Conversion. autodestruct; repeat pseudo_step. + Local Notation "v [[ i ]]" := (nth i v (wzero _)) (at level 40). + Local Notation "$$ v" := (natToWord _ v) (at level 40). + Definition convert_example: @pseudeq 32 W32 1 1 (fun v => - Let_In (natToWord _ 1) (fun a => - Let_In (nth 0 v (wzero _)) (fun b => - [a ^& b]))). + Let_In ($$ 1) (fun a => + Let_In (v[[0]]) (fun b => [ + a ^& b + ]))). pseudo_solve. Defined. |