From 6ea5d70f608ec5b3aea485843e677ce84ace6648 Mon Sep 17 00:00:00 2001
From: Robert Sloan <varomodt@gmail.com>
Date: Thu, 23 Jun 2016 00:21:52 -0400
Subject: Pseudize Let_In with minor notations

---
 src/Assembly/Pseudize.v | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

(limited to 'src/Assembly')

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.
-- 
cgit v1.2.3