diff options
| -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. |