Tuple-ization tactics work

Most of Medial, less the conversions

Most of Medial, less the conversions

Most of Medial, less the conversions

Most of Medial, less the conversions

More of Medial

MedialConversions done

1 files changed, 20 insertions, 20 deletions

diff --git a/src/Assembly/QhasmEvalCommon.v b/src/Assembly/QhasmEvalCommon.v
index cc0b7c63b..b6261d1c6 100644
--- a/src/Assembly/QhasmEvalCommon.v
+++ b/src/Assembly/QhasmEvalCommon.v
@@ -35,29 +35,29 @@ Definition evalCond (c: Conditional) (state: State): option bool :=
     end
   end.
 
-Definition evalOperation (o: Operation) (state: State): option State :=
-  let evalIOp := fun {b} (io: IntOp) (x y: word b) =>
-    match io with
-    | IPlus => wplus x y
-    | IMinus => wminus x y
-    | IXor => wxor x y
-    | IAnd => wand x y
-    | IOr => wor x y
-    end in
+Definition evalIOp {b} (io: IntOp) (x y: word b) :=
+  match io with
+  | IPlus => wplus x y
+  | IMinus => wminus x y
+  | IXor => wxor x y
+  | IAnd => wand x y
+  | IOr => wor x y
+  end.
 
-  let evalRotOp := fun {b} (ro: RotOp) (x: word b) (n: nat) =>
-    match ro with
-    | Shl => NToWord b (N.shiftl_nat (wordToN x) n)
-    | Shr => NToWord b (N.shiftr_nat (wordToN x) n)
-    end in
+Definition evalRotOp {b} (ro: RotOp) (x: word b) (n: nat) :=
+  match ro with
+  | Shl => NToWord b (N.shiftl_nat (wordToN x) n)
+  | Shr => NToWord b (N.shiftr_nat (wordToN x) n)
+  end.
 
-  let evalDualOp := fun {b} (duo: DualOp) (x y: word b) =>
-    match duo with
-    | IMult =>
-      let wres := natToWord (b + b) (N.to_nat ((wordToN x) * (wordToN y))) in
-      (split1 b b wres, split2 b b wres)
-    end in
+Definition evalDualOp {b} (duo: DualOp) (x y: word b) :=
+  match duo with
+  | IMult =>
+    let wres := natToWord (b + b) (N.to_nat ((wordToN x) * (wordToN y))) in
+    (split1 b b wres, split2 b b wres)
+  end.
 
+Definition evalOperation (o: Operation) (state: State): option State :=
   let liftOpt := fun {A B C} (f: A -> B -> option C) (xo: option A) (yo: option B) =>
     match (xo, yo) with
     | (Some x, Some y) => f x y