Update the syntax of the pretty-printed let equalities

Author: sonmarcho

backends/lean/Aeneas/Progress/Progress.lean

@@ -14,12 +14,12 @@ open Utils
 /-- A special definition that we use to introduce pretty-printed terms in the context -/
 def prettyMonadEq {α : Type u} (x : Std.Result α) (y : α) : Prop := x = .ok y
 
-macro:max "[> " "let" y:term " ← " x:term    : term => `(prettyMonadEq $x $y)
+macro:max "[> " "let" y:term " ← " x:term " <]"   : term => `(prettyMonadEq $x $y)
 
 @[app_unexpander prettyMonadEq]
-def unexpPrettyMonadEqofNat : Lean.PrettyPrinter.Unexpander | `($_ $x $y) => `([> let $y ← $x) | _ => throw ()
+def unexpPrettyMonadEqofNat : Lean.PrettyPrinter.Unexpander | `($_ $x $y) => `([> let $y ← $x <]) | _ => throw ()
 
-example (x y z : Std.U32) (_ : [> let z ← (x + y)) : True := by simp
+example (x y z : Std.U32) (_ : [> let z ← (x + y) <]) : True := by simp
 
 theorem eq_imp_prettyMonadEq {α : Type u} {x : Std.Result α} {y : α} (h : x = .ok y) : prettyMonadEq x y := by simp [prettyMonadEq, h]
 
@@ -612,7 +612,7 @@ info: example
   (y : UScalar ty)
   (h : ↑x + ↑y ≤ UScalar.max ty)
   (z : UScalar ty)
-  (_ : [> let z ← x + y)
+  (_ : [> let z ← x + y <])
   (h1 : ↑z = ↑x + ↑y) :
   ↑z = ↑x + ↑y
   := by sorry
@@ -632,10 +632,10 @@ info: example
   (y : UScalar ty)
   (h : 2 * ↑x + ↑y ≤ UScalar.max ty)
   (z1 : UScalar ty)
-  (__1 : [> let z1 ← x + y)
+  (__1 : [> let z1 ← x + y <])
   (h1 : ↑z1 = ↑x + ↑y)
   (z2 : UScalar ty)
-  (_ : [> let z2 ← z1 + x)
+  (_ : [> let z2 ← z1 + x <])
   (h2 : ↑z2 = ↑z1 + ↑x) :
   ↑z2 = 2 * ↑x + ↑y
   := by sorry

backends/lean/Aeneas/Progress/ProgressStar.lean

@@ -445,7 +445,7 @@ b : Bool
 x y : U32
 h✝ : b = true
 x2 : U32
-_ : [> let x2 ← x + y
+_ : [> let x2 ← x + y <]
 x2_post : ↑x2 = ↑x + ↑y
 ⊢ ↑x2 + ↑x2 ≤ U32.max
 
@@ -454,10 +454,10 @@ b : Bool
 x y : U32
 h✝ : b = true
 x2 : U32
-_✝ : [> let x2 ← x + y
+_✝ : [> let x2 ← x + y <]
 x2_post : ↑x2 = ↑x + ↑y
 x3 : U32
-_ : [> let x3 ← x2 + x2
+_ : [> let x3 ← x2 + x2 <]
 x3_post : ↑x3 = ↑x2 + ↑x2
 ⊢ ↑x3 + ↑4#u32 ≤ U32.max
 
@@ -472,7 +472,7 @@ b : Bool
 x y✝ : U32
 h✝ : ¬b = true
 y : U32
-_ : [> let y ← x + y✝
+_ : [> let y ← x + y✝ <]
 y_post : ↑y = ↑x + ↑y✝
 ⊢ ↑y + ↑2#u32 ≤ U32.max
 -/