diff --git a/CHANGELOG.md b/CHANGELOG.md
index a5054c505..b96ada003 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -34,6 +34,9 @@ Changes to the frontend:
 Changes to hax-lib:
 - New behavior for `hax_lib::include`: it now forces inclusion when in contradiction with `-i` flag.
 
+Changes to the Lean backend:
+- Improve support for functionalized loops (#1695)
+
 Miscellaneous:
  - A lean tutorial has been added to the hax website (#1626)
  - Diagnostics reporting were improved (#1692)
diff --git a/engine/lib/phases/phase_rewrite_control_flow.ml b/engine/lib/phases/phase_rewrite_control_flow.ml
index d97f0b275..c237fa01c 100644
--- a/engine/lib/phases/phase_rewrite_control_flow.ml
+++ b/engine/lib/phases/phase_rewrite_control_flow.ml
@@ -72,7 +72,7 @@ module Make (F : Features.T) =
               let arms =
                 [
                   MS.arm
-                    (mk_cf_pat `Break (U.make_var_pat id typ span))
+                    (mk_cf_pat `Break (U.make_var_pat id return_type span))
                     return_expr;
                   MS.arm (mk_cf_pat `Continue pat)
                     (U.make_lets stmts_after final |> self#visit_expr in_loop);
diff --git a/examples/lean_barrett/Makefile b/examples/lean_barrett/Makefile
index 66e0376b0..5a3f7e965 100644
--- a/examples/lean_barrett/Makefile
+++ b/examples/lean_barrett/Makefile
@@ -3,7 +3,6 @@ default:
 	cargo hax into lean
 	(cd proofs/lean/extraction && \
    elan default stable && \
-   lake update && \
    lake build)
 
 clean:
diff --git a/examples/lean_barrett/proofs/lean/extraction/lean-toolchain b/examples/lean_barrett/proofs/lean/extraction/lean-toolchain
new file mode 100644
index 000000000..1f2f20aae
--- /dev/null
+++ b/examples/lean_barrett/proofs/lean/extraction/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.22.0
\ No newline at end of file
diff --git a/examples/lean_chacha20/Makefile b/examples/lean_chacha20/Makefile
index 0ba9b292f..c7b8c1743 100644
--- a/examples/lean_chacha20/Makefile
+++ b/examples/lean_chacha20/Makefile
@@ -3,7 +3,6 @@ default:
 	cargo hax into lean
 	(cd proofs/lean/extraction && \
    elan default stable && \
-   lake update && \
    lake build)
 
 clean:
diff --git a/examples/lean_chacha20/proofs/lean/extraction/Lean_chacha20_manual_edit.lean b/examples/lean_chacha20/proofs/lean/extraction/Lean_chacha20_manual_edit.lean
index 7f06f6123..f9926373c 100644
--- a/examples/lean_chacha20/proofs/lean/extraction/Lean_chacha20_manual_edit.lean
+++ b/examples/lean_chacha20/proofs/lean/extraction/Lean_chacha20_manual_edit.lean
@@ -614,36 +614,14 @@ def Lean_chacha20.chacha20  (m : (RustSlice u8))
 theorem Lean_chacha20.Hacspec_helper.add_state_spec (state : (Vector u32 16)) (other : (Vector u32 16)) :
   ⦃ ⌜ True ⌝ ⦄
   (Lean_chacha20.Hacspec_helper.add_state state other)
-  ⦃ ⇓ _ => True ⦄ := by
-  mvcgen [Lean_chacha20.Hacspec_helper.add_state]
-  <;> try apply SPred.pure_intro
-  <;> simp [Vector.size] at *
-  <;> cases System.Platform.numBits_eq with
-    | inl h
-    | inr h =>
-      expose_names
-      rw [h]
-      omega
+  ⦃ ⇓ _ => True ⦄ := by sorry
 
 @[spec]
 theorem Lean_chacha20.Hacspec_helper.to_le_u32s_16_spec bytes :
   bytes.size = 64 →
   ⦃ ⌜ True ⌝ ⦄
   (Lean_chacha20.Hacspec_helper.to_le_u32s_16 bytes)
-  ⦃ ⇓ _ => True ⦄ := by
-  intro
-  open SpecNat in
-  mvcgen [Lean_chacha20.Hacspec_helper.to_le_u32s_16]
-  <;> (try apply SPred.pure_intro)
-  all_goals simp [USize.size, Vector.size] at *
-  any_goals subst_vars
-  all_goals try simp [USize.le_iff_toNat_le]
-  all_goals try (cases System.Platform.numBits_eq with
-    | inl h
-    | inr h =>
-      expose_names
-      rw [h]
-      omega ; done )
+  ⦃ ⇓ _ => True ⦄ := by sorry
 
 
 @[spec]
@@ -651,19 +629,7 @@ theorem Lean_chacha20.Hacspec_helper.to_le_u32s_3_spec bytes :
   bytes.size = 12 →
   ⦃ ⌜ True ⌝ ⦄
   (Lean_chacha20.Hacspec_helper.to_le_u32s_3 bytes)
-  ⦃ ⇓ _ => True ⦄ := by
-  intros
-  open SpecNat in
-  mvcgen [Lean_chacha20.Hacspec_helper.to_le_u32s_3]
-  all_goals simp [USize.size, RustArray, Vector.size] at *
-  any_goals subst_vars
-  all_goals try simp [USize.le_iff_toNat_le]
-  all_goals try (cases System.Platform.numBits_eq with
-    | inl h
-    | inr h =>
-      expose_names
-      rw [h]
-      omega ; done )
+  ⦃ ⇓ _ => True ⦄ := by sorry
 
 
 
@@ -672,59 +638,19 @@ theorem Lean_chacha20.Hacspec_helper.to_le_u32s_8_spec (bytes : (Array u8)) :
   bytes.size = 32 →
   ⦃ ⌜ True ⌝ ⦄
   ( Lean_chacha20.Hacspec_helper.to_le_u32s_8 bytes )
-  ⦃ ⇓ _ => True ⦄ := by
-  intros
-  open SpecNat in
-  mvcgen [Lean_chacha20.Hacspec_helper.to_le_u32s_8]
-  all_goals simp [USize.size, Vector.size] at *
-  any_goals subst_vars
-  all_goals try simp [USize.le_iff_toNat_le]
-  all_goals try (cases System.Platform.numBits_eq with
-    | inl h
-    | inr h =>
-      expose_names
-      rw [h]
-      omega ; done )
+  ⦃ ⇓ _ => True ⦄ := by sorry
 
 @[spec]
 theorem Lean_chacha20.Hacspec_helper.u32s_to_le_bytes_spec (state : (Vector u32 16)) :
   ⦃ ⌜ True ⌝ ⦄
   (Lean_chacha20.Hacspec_helper.u32s_to_le_bytes state)
-  ⦃ ⇓ _ => True ⦄ := by
-  intros
-  open SpecNat in
-  mvcgen [Lean_chacha20.Hacspec_helper.u32s_to_le_bytes, Core.Num.Impl_8.to_le_bytes]
-  all_goals simp [USize.size, Vector.size] at *
-  any_goals subst_vars
-  all_goals try simp [USize.toNat_ofNat'] at *
-  all_goals try (cases System.Platform.numBits_eq with
-    | inl h
-    | inr h =>
-      expose_names
-      rw [h] ;
-      try rw [h] at h_2
-      try rw [h] at h_3
-      try rw [h] at h_5
-      omega ; done )
+  ⦃ ⇓ _ => True ⦄ := by sorry
 
 @[spec]
 theorem Lean_chacha20.Hacspec_helper.xor_state_spec (state other: (Vector u32 16)) :
   ⦃ ⌜ True ⌝ ⦄
   (Lean_chacha20.Hacspec_helper.xor_state state other)
-  ⦃ ⇓ _ => True ⦄ := by
-  intros
-  open SpecNat in
-  mvcgen [Lean_chacha20.Hacspec_helper.xor_state,
-    Core.Num.Impl_8.to_le_bytes]
-  all_goals simp [Vector.size] at *
-  any_goals subst_vars
-  all_goals try simp at *
-  all_goals try (cases System.Platform.numBits_eq with
-    | inl h
-    | inr h =>
-      expose_names
-      rw [h] ;
-      omega ; done )
+  ⦃ ⇓ _ => True ⦄ := by sorry
 
 
 @[spec]
@@ -732,21 +658,7 @@ theorem Lean_chacha20.Hacspec_helper.update_array_spec (a: (Vector u8 64)) (v: A
   v.size ≤ 64 →
   ⦃ ⌜ True ⌝ ⦄
   (Lean_chacha20.Hacspec_helper.update_array a v)
-  ⦃ ⇓ _ => True ⦄ := by
-  intros
-  open SpecNat in
-  mvcgen_step 24 [Lean_chacha20.Hacspec_helper.update_array]
-  all_goals simp [Vector.size, USize.le_iff_toNat_le] at *
-  any_goals subst_vars
-  all_goals try simp [USize.toNat_ofNat'] at *
-  all_goals try (cases System.Platform.numBits_eq with
-    | inl h
-    | inr h =>
-      expose_names
-      try rw [h] ;
-      try rw [h] at h_2
-      try rw [h] at h_4
-      omega ; done )
+  ⦃ ⇓ _ => True ⦄ := by sorry
 
 @[spec]
 theorem Lean_chacha20.chacha20_line_spec
@@ -784,8 +696,7 @@ theorem Lean_chacha20.chacha20_double_round_spec (state : (Vector u32 16)) :
 theorem Lean_chacha20.chacha20_rounds_spec state :
   ⦃ ⌜ True ⌝ ⦄
   (Lean_chacha20.chacha20_rounds state)
-  ⦃ ⇓ _ => True ⦄ := by
-  mvcgen [Lean_chacha20.chacha20_rounds]
+  ⦃ ⇓ _ => True ⦄ := by sorry
 
 
 @[spec]
@@ -850,25 +761,7 @@ theorem Lean_chacha20.chacha20_update_spec (st0 : (Vector u32 16)) (m : (Array u
   ⦃ m.size ≤ USize.size ⦄
   (Lean_chacha20.chacha20_update st0 m)
   ⦃ ⇓ _ => True ⦄
-:= by
-  open SpecNat in
-  mvcgen [Lean_chacha20.chacha20_update,
-    Alloc.Slice.Impl.to_vec,
-    Core.Result.Impl.unwrap.spec,
-    Alloc.Vec.Impl.new,
-    Alloc.Vec.Impl_1.len,
-    ] <;> subst_vars
-  all_goals simp [Array.size_extract, USize.eq_iff_toBitVec_eq, BitVec.toNat_eq, USize.size, USize.le_iff_toNat_le ] at *
-  all_goals try cases System.Platform.numBits_eq with
-    | inl h
-    | inr h =>
-      expose_names
-      try rw [h]
-      try rw [h] at h_1
-      try rw [h] at h_2
-      try rw [h] at h_3
-      try rw [h] at h_4
-      omega ; done
+:= by sorry
 
 theorem Lean_chacha20.chacha20_spec
   (m : (Array u8)) (key : (Vector u8 32)) (iv : (Vector u8 12)) (ctr : u32) :
diff --git a/examples/lean_chacha20/proofs/lean/extraction/lean-toolchain b/examples/lean_chacha20/proofs/lean/extraction/lean-toolchain
new file mode 100644
index 000000000..8ce10238f
--- /dev/null
+++ b/examples/lean_chacha20/proofs/lean/extraction/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.22.0-rc4
\ No newline at end of file
diff --git a/hax-lib/proof-libs/lean/Hax/Lib.lean b/hax-lib/proof-libs/lean/Hax/Lib.lean
index 6afed31b7..f0d159617 100644
--- a/hax-lib/proof-libs/lean/Hax/Lib.lean
+++ b/hax-lib/proof-libs/lean/Hax/Lib.lean
@@ -911,24 +911,24 @@ section RustResult
 namespace Core.Result
 
 inductive Result α β
-| ok : α -> Result α β
-| err : β -> Result α β
+| Ok : α -> Result α β
+| Err : β -> Result α β
 
 instance {β : Type} : Monad (fun α => Result α β) where
-  pure x := .ok x
+  pure x := .Ok x
   bind {α α'} x (f: α -> Result α' β) := match x with
-  | .ok v => f v
-  | .err e => .err e
+  | .Ok v => f v
+  | .Err e => .Err e
 
 /-- Rust unwrapping, panics if `x` is not `result.Result.ok _` -/
 def Impl.unwrap (α: Type) (β:Type) (x: Result α β) :=
   match x with
-  | .err _ => Result.fail .panic
-  | .ok v => pure v
+  | .Err _ => Result.fail .panic
+  | .Ok v => pure v
 
 @[spec]
 theorem Impl.unwrap.spec {α β} (x: Result α β) v :
-  x = Result.ok v →
+  x = Result.Ok v →
   ⦃ True ⦄
   (Impl.unwrap α β x)
   ⦃ ⇓ r => r = v ⦄ := by
@@ -956,61 +956,61 @@ loop `body` from index `e` to `s`. If the invariant is not checked at runtime,
 only passed around
 
 -/
-def Rust_primitives.Hax.Folds.fold_range {α}
-  (s e : Nat)
-  (inv : α -> Nat -> Result Bool)
-  (init: α)
-  (body : α -> Nat -> Result α) : Result α := do
-  if e ≤ s then pure init
-  else Rust_primitives.Hax.Folds.fold_range (s+1) e inv (← body init s) body
-
--- Lemma for proof of hax_folds_fold_range property
-private
-theorem induction_decreasing {e} {P: Nat  → Prop}
-  (init: P e)
-  (rec: ∀ n, n < e → P (n+1) → P n) :
-  ∀ n, n ≤ e → P n
-:= by
-  intros n h
-  by_cases (n = 0)
-  . subst_vars
-    induction e <;> try grind
-  generalize h: (e - n) = d
-  have : n = e - d := by omega
-  have hlt : d < e := by omega
-  rw [this] ; clear h this
-  induction d with
-  | zero => simp ; grind
-  | succ d ih =>
-    apply rec <;> try omega
-    suffices e - (d + 1) + 1 = e - d by grind
-    omega
 
--- Lemma for proof of hax_folds_fold_range property
-private
-def induction_decreasing_range {s e} {P: Nat → Nat → Prop} :
-  s ≤ e →
-  (init: P e e) →
-  (rec: ∀ (n : Nat), n < e → s ≤ n → P (n + 1) e → P n e) →
-  P s e
-:= by intros; apply induction_decreasing (P := fun n => (s ≤ n → P n e)) (e := e) <;> try grind
+inductive Core.Ops.Control_flow.ControlFlow (α β: Type 0) where
+| Break (x: α)
+| Continue (y : β)
+open Core.Ops.Control_flow
+
+class Rust_primitives.Hax.Folds {int_type: Type} where
+  fold_range {α : Type}
+    (s e : int_type)
+    (inv : α -> int_type -> Result Bool)
+    (init: α)
+    (body : α -> int_type -> Result α)
+    : Result α
+  fold_range_return  {α_acc α_ret : Type}
+    (s e: int_type)
+    (inv : α_acc -> int_type -> Result Bool)
+    (init: α_acc)
+    (body : α_acc -> int_type ->
+      Result (ControlFlow (ControlFlow α_ret (Tuple2 Tuple0 α_acc)) α_acc ))
+    : Result (ControlFlow α_ret α_acc)
+
+instance : Coe Nat Nat where
+  coe x := x
 
-/--
+@[simp, spec]
+instance {α} [Coe α Nat] [Coe Nat α]: @Rust_primitives.Hax.Folds α where
+  fold_range s e inv init body := do
+    let mut acc := init
+    for i in [s:e] do
+      acc := (← body acc i)
+    return acc
+
+  fold_range_return {α_acc α_ret} s e inv init body := do
+    let mut acc := init
+    for i in [s:e] do
+      match (← body acc i) with
+      | .Break (.Break res ) => return (.Break res)
+      | .Break (.Continue ⟨ ⟨ ⟩, res⟩) => return (.Continue res)
+      | .Continue acc' => acc := acc'
+    pure (ControlFlow.Continue acc)
 
+/-
 Nat-based specification for hax_folds_fold_range. It requires that the invariant
 holds on the initial value, and that for any index `i` between the start and end
 values, executing body of the loop on a value that satisfies the invariant
 produces a result that also satisfies the invariant.
 
 -/
-@[spec]
 theorem Rust_primitives.Hax.Folds.fold_range_spec {α}
   (s e : Nat)
   (inv : α -> Nat -> Result Bool)
   (init: α)
   (body : α -> Nat -> Result α) :
-  inv init s = pure true →
   s ≤ e →
+  inv init s = pure true →
   (∀ (acc:α) (i:Nat),
     s ≤ i →
     i < e →
@@ -1022,22 +1022,29 @@ theorem Rust_primitives.Hax.Folds.fold_range_spec {α}
   (Rust_primitives.Hax.Folds.fold_range s e inv init body)
   ⦃ ⇓ r => inv r e = pure true ⦄
 := by
-  intro h_inv_s h_s_le_e h_body
-  revert h_inv_s init
-  apply induction_decreasing_range (s := s) (e := e) <;> try grind
-  . intros
-    unfold Rust_primitives.Hax.Folds.fold_range
-    mvcgen
+  intro h_inv_s h_le h_body
+  mvcgen [Spec.forIn_list]
+  case inv =>
+    simp [Coe.coe]
+    exact PostCond.total
+      (fun (acc , ⟨suff, _, _ ⟩) => inv acc (s + suff.length) = pure true )
+  case step =>
+    simp at h
+    expose_names
+    rw [Std.Range.toList_range'] at *
+    case h => simp
+    have ⟨k ,⟨ h_k, h_pre, h_suff⟩⟩ := List.range'_eq_append_iff.mp h_1
+    let h_suff := Eq.symm h_suff
+    let ⟨ h_x ,_ , h_suff⟩ := List.range'_eq_cons_iff.mp h_suff
+    mspec h_body <;> simp [Coe.coe] at * <;> try omega
+    . rw [← List.length_reverse, h_pre, List.length_range', h_x] at h; assumption
+    . rw [← List.length_reverse, h_pre, List.length_range', ← Nat.add_assoc, h_x]
+      intro; assumption
+  all_goals simp at *
+  case pre1 =>  assumption
+  case post.success =>
+    suffices (s + (e - s)) = e by (rw [← this]; assumption)
     omega
-  . intros n _ _ ih acc h_acc
-    unfold Rust_primitives.Hax.Folds.fold_range
-    mvcgen <;> (try grind) <;> try omega
-    specialize h_body acc n (by omega) (by omega)
-    mspec h_body
-    . assumption
-    . intro h_r
-      apply (ih _ h_r)
-      grind
 
 end Fold
 
@@ -1090,9 +1097,9 @@ def Core.Convert.TryInto.try_into {α n} (a: Array α) :
    Result (Core.Result.Result (Vector α n) Core.Array.TryFromSliceError) :=
    pure (
      if h: a.size = n then
-       Core.Result.Result.ok (Eq.mp (congrArg _ h) a.toVector)
+       Core.Result.Result.Ok (Eq.mp (congrArg _ h) a.toVector)
      else
-       .err .array.TryFromSliceError
+       .Err .array.TryFromSliceError
      )
 
 @[spec]
@@ -1100,7 +1107,7 @@ theorem Core.Convert.TryInto.try_into.spec {α n} (a: Array α) :
   (h: a.size = n) →
   ⦃ True ⦄
   ( Core.Convert.TryInto.try_into a)
-  ⦃ ⇓ r => r = .ok (Eq.mp (congrArg _ h) a.toVector) ⦄ := by
+  ⦃ ⇓ r => r = .Ok (Eq.mp (congrArg _ h) a.toVector) ⦄ := by
   intro h
   mvcgen [Core.Result.Impl.unwrap.spec, Core.Convert.TryInto.try_into]
   apply SPred.pure_intro
@@ -1300,12 +1307,12 @@ abbrev RustVector := Array
 
 def Alloc.Alloc.Global : Type := Unit
 
-def Alloc.Vec.Vec (α: Type) (_Allocator:Type) : Type := Array α
+abbrev Alloc.Vec.Vec (α: Type) (_Allocator:Type) : Type := Array α
 
 def Alloc.Vec.Impl.new (α: Type) (_:Tuple0) : Result (Alloc.Vec.Vec α Alloc.Alloc.Global) :=
   pure ((List.nil).toArray)
 
-def Alloc.Vec.Impl_1.len (α: Type) (_Allocator: Type) (x: Alloc.Vec.Vec α Alloc.Alloc.Global) : Result Nat :=
+def Alloc.Vec.Impl_1.len (α: Type) (_Allocator: Type) (x: Alloc.Vec.Vec α Alloc.Alloc.Global) : Result usize :=
   pure x.size
 
 def Alloc.Vec.Impl_2.extend_from_slice α (_Allocator: Type) (x: Alloc.Vec.Vec α Alloc.Alloc.Global) (y: Array α)
diff --git a/rust-engine/src/backends/lean.rs b/rust-engine/src/backends/lean.rs
index 26da17bb2..633cbaac9 100644
--- a/rust-engine/src/backends/lean.rs
+++ b/rust-engine/src/backends/lean.rs
@@ -189,22 +189,6 @@ impl LeanPrinter {
             .clone();
         self.escape(id)
     }
-
-    /// Renders expressions with an explicit ascription `(e : Result ty)`. Used for the body of closure, for
-    /// numeric literals, etc.
-    fn expr_typed_result<'a, 'b, A: 'a + Clone>(
-        &'a self,
-        expr: &'b Expr,
-    ) -> DocBuilder<'a, Self, A> {
-        macro_rules! line {($($tt:tt)*) => {disambiguated_line!($($tt)*)};}
-        install_pretty_helpers!(self: Self);
-        docs![
-            expr,
-            reflow!(" : "),
-            docs!["Result", line!(), &expr.ty].group()
-        ]
-        .group()
-    }
 }
 
 /// Render parameters, adding a line after each parameter
@@ -298,6 +282,26 @@ const _: () = {
         ) -> DocBuilder<'a, Self, A> {
             zip_right!(params, line!())
         }
+
+        /// Renders expressions with an explicit ascription `(e : Result ty)`. Used for the body of closure, for
+        /// numeric literals, etc.
+        fn expr_typed_result<'a, 'b, A: 'a + Clone>(
+            &'a self,
+            expr: &'b Expr,
+        ) -> DocBuilder<'a, Self, A> {
+            docs![
+                expr,
+                reflow!(" : "),
+                docs!["Result", line!(), &expr.ty].group()
+            ]
+            .group()
+        }
+
+        fn pat_typed<'a, 'b, A: 'a + Clone>(&'a self, pat: &'b Pat) -> DocBuilder<'a, Self, A> {
+            docs![pat.kind(), reflow!(" :"), line!(), &pat.ty]
+                .parens()
+                .group()
+        }
     }
 
     impl<'a, 'b, A: 'a + Clone> PrettyAst<'a, 'b, A> for LeanPrinter {
@@ -382,10 +386,6 @@ set_option linter.unusedVariables false
             }
         }
 
-        fn pat(&'a self, pat: &'b Pat) -> DocBuilder<'a, Self, A> {
-            docs![&*pat.kind, reflow!(" : "), &pat.ty].parens().group()
-        }
-
         fn expr(&'a self, Expr { kind, ty, meta: _ }: &'b Expr) -> DocBuilder<'a, Self, A> {
             match &**kind {
                 ExprKind::Literal(int_lit @ Literal::Int { .. }) => {
@@ -567,12 +567,18 @@ set_option linter.unusedVariables false
                     }
                 },
                 ExprKind::Match { scrutinee, arms } => docs![
-                    docs!["match", line!(), scrutinee, reflow!(" with")].group(),
-                    line!(),
-                    intersperse!(arms, line!())
+                    docs![
+                        "match",
+                        docs![line!(), scrutinee].nest(INDENT),
+                        line!(),
+                        "with"
+                    ]
+                    .group(),
+                    docs![line!(), intersperse!(arms, line!())]
+                        .group()
+                        .nest(INDENT),
                 ]
                 .parens()
-                .nest(INDENT)
                 .group(),
                 _ => todo!(),
             }
@@ -593,6 +599,10 @@ set_option linter.unusedVariables false
             }
         }
 
+        fn pat(&'a self, pat: &'b Pat) -> DocBuilder<'a, Self, A> {
+            docs![pat.kind()]
+        }
+
         fn pat_kind(&'a self, pat_kind: &'b PatKind) -> DocBuilder<'a, Self, A> {
             match pat_kind {
                 PatKind::Wild => docs!["_"],
@@ -688,7 +698,7 @@ set_option linter.unusedVariables false
                     let kind = impl_.kind();
                     match &kind {
                         ImplExprKind::Self_ => docs![self.render_last(item)],
-                        _ => todo!("sorry \n-- support only local associated types\n"), // Support only local associated types
+                        _ => todo!(), // Support only local associated types
                     }
                 }
                 _ => todo!("sorry \n-- unsupported type\n"),
@@ -773,7 +783,7 @@ set_option linter.unusedVariables false
         }
 
         fn param(&'a self, param: &'b Param) -> DocBuilder<'a, Self, A> {
-            docs![&param.pat]
+            self.pat_typed(&param.pat)
         }
 
         fn item(
@@ -1024,7 +1034,7 @@ set_option linter.unusedVariables false
                         name,
                         softline!(),
                         generics,
-                        zip_right!(params, line!()).group().align(),
+                        zip_right!(params, line!()).group(),
                         ":= do",
                     ]
                     .group(),
diff --git a/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap b/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap
index 0f62729a7..7e7c2b73f 100644
--- a/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap	
+++ b/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap	
@@ -69,7 +69,7 @@ def Lean_tests.Traits.Overlapping_methods.test
   (_ : Rust_primitives.Hax.Tuple0)
   : Result usize
   := do
-  let (x : u32) ← (pure (9 : u32));
+  let x ← (pure (9 : u32));
   (← (← (← Lean_tests.Traits.Overlapping_methods.T1.f x)
       +? (← Lean_tests.Traits.Overlapping_methods.T2.f x))
     +? (← Lean_tests.Traits.Overlapping_methods.T3.f x))
@@ -166,7 +166,7 @@ instance Lean_tests.Traits.Bounds.Impl_2 :
   Lean_tests.Traits.Bounds.S1
   where
   f_test (self : Lean_tests.Traits.Bounds.S2)
-         (x : Lean_tests.Traits.Bounds.S1)
+    (x : Lean_tests.Traits.Bounds.S1)
     := do
     (← (← (← Lean_tests.Traits.Bounds.T1.f1 x)
         +? (← Lean_tests.Traits.Bounds.T2.f2 self))
@@ -192,7 +192,7 @@ instance Lean_tests.Traits.Basic.Impl :
   where
   f1 (self : Lean_tests.Traits.Basic.S) := do (42 : usize)
   f2 (self : Lean_tests.Traits.Basic.S)
-     (other : Lean_tests.Traits.Basic.S)
+    (other : Lean_tests.Traits.Basic.S)
     := do
     (43 : usize)
 
@@ -320,71 +320,33 @@ def Lean_tests.Structs.tuple_structs
       (Lean_tests.Structs.T2.mk
         (Lean_tests.Structs.T1.mk (1 : i32))
         (Lean_tests.Structs.T2.mk (1 : i32) (2 : i32)))));
-  let (⟨⟩ : Lean_tests.Structs.T0) ← (pure t0);
-  let (⟨(u1 : i32)⟩ : (Lean_tests.Structs.T1 i32)) ← (pure t1);
-  let (⟨(u2 : i32), (u3 : i32)⟩ : (Lean_tests.Structs.T2 i32 i32)) ← (pure t2);
-  let
-    (⟨(⟨⟩ : Lean_tests.Structs.T0),
-      (⟨(_ : i32)⟩ : (Lean_tests.Structs.T1 i32)),
-      (⟨(_ : i32), (_ : i32)⟩ : (Lean_tests.Structs.T2 i32 i32))⟩ :
-    (Lean_tests.Structs.T3
-      Lean_tests.Structs.T0
-      (Lean_tests.Structs.T1 i32)
-      (Lean_tests.Structs.T2 i32 i32))) ← (pure t3);
-  let
-    (⟨(⟨⟩ : Lean_tests.Structs.T0),
-      (⟨(⟨(_ : i32)⟩ : (Lean_tests.Structs.T1 i32)),
-        (⟨(_ : i32), (_ : i32)⟩ : (Lean_tests.Structs.T2 i32 i32))⟩ :
-      (Lean_tests.Structs.T2
-        (Lean_tests.Structs.T1 i32)
-        (Lean_tests.Structs.T2 i32 i32)))⟩ : (Lean_tests.Structs.T3p
-      Lean_tests.Structs.T0
-      (Lean_tests.Structs.T1 i32)
-      (Lean_tests.Structs.T2 i32 i32))) ← (pure t3p);
-  let (_ : i32) ← (pure (Lean_tests.Structs.T1._0 t1));
-  let (_ : i32) ← (pure (Lean_tests.Structs.T2._0 t2));
-  let (_ : i32) ← (pure (Lean_tests.Structs.T2._1 t2));
-  let (_ : Lean_tests.Structs.T0) ← (pure (Lean_tests.Structs.T3._0 t3));
-  let (_ : (Lean_tests.Structs.T1 i32)) ← (pure (Lean_tests.Structs.T3._1 t3));
-  let (_ : (Lean_tests.Structs.T2 i32 i32)) ← (pure
-    (Lean_tests.Structs.T3._2 t3));
-  let (_ : i32) ← (pure
-    (Lean_tests.Structs.T2._1 (Lean_tests.Structs.T3._2 t3)));
-  let (_ : Lean_tests.Structs.T0) ← (pure (Lean_tests.Structs.T3p._0 t3p));
-  let
-    (_ : (Lean_tests.Structs.T2
-      (Lean_tests.Structs.T1 i32)
-      (Lean_tests.Structs.T2 i32 i32))) ← (pure
-    (Lean_tests.Structs.T3p._1 t3p));
-  let (_ : i32) ← (pure
+  let ⟨⟩ ← (pure t0);
+  let ⟨u1⟩ ← (pure t1);
+  let ⟨u2, u3⟩ ← (pure t2);
+  let ⟨⟨⟩, ⟨_⟩, ⟨_, _⟩⟩ ← (pure t3);
+  let ⟨⟨⟩, ⟨⟨_⟩, ⟨_, _⟩⟩⟩ ← (pure t3p);
+  let _ ← (pure (Lean_tests.Structs.T1._0 t1));
+  let _ ← (pure (Lean_tests.Structs.T2._0 t2));
+  let _ ← (pure (Lean_tests.Structs.T2._1 t2));
+  let _ ← (pure (Lean_tests.Structs.T3._0 t3));
+  let _ ← (pure (Lean_tests.Structs.T3._1 t3));
+  let _ ← (pure (Lean_tests.Structs.T3._2 t3));
+  let _ ← (pure (Lean_tests.Structs.T2._1 (Lean_tests.Structs.T3._2 t3)));
+  let _ ← (pure (Lean_tests.Structs.T3p._0 t3p));
+  let _ ← (pure (Lean_tests.Structs.T3p._1 t3p));
+  let _ ← (pure
     (Lean_tests.Structs.T2._0
         (Lean_tests.Structs.T2._1 (Lean_tests.Structs.T3p._1 t3p))));
-  let (_ : (Lean_tests.Structs.T1 i32)) ← (pure
-    (Lean_tests.Structs.T2._0 (Lean_tests.Structs.T3p._1 t3p)));
-  let (_ : (Lean_tests.Structs.T2 i32 i32)) ← (pure
-    (Lean_tests.Structs.T2._1 (Lean_tests.Structs.T3p._1 t3p)));
-  let (_ : Rust_primitives.Hax.Tuple0) ← (pure
-    (match t0 with | ⟨⟩ => do Rust_primitives.Hax.Tuple0.mk));
-  let (_ : Rust_primitives.Hax.Tuple0) ← (pure
-    (match t1 with | ⟨(u1 : i32)⟩ => do Rust_primitives.Hax.Tuple0.mk));
-  let (_ : Rust_primitives.Hax.Tuple0) ← (pure
-    (match t2 with
-      | ⟨(u2 : i32), (u3 : i32)⟩ => do Rust_primitives.Hax.Tuple0.mk));
-  let (_ : Rust_primitives.Hax.Tuple0) ← (pure
-    (match t3 with
-      | ⟨(⟨⟩ : Lean_tests.Structs.T0),
-         (⟨(u1 : i32)⟩ : (Lean_tests.Structs.T1 i32)),
-         (⟨(u2 : i32), (u3 : i32)⟩ : (Lean_tests.Structs.T2 i32 i32))⟩
-        => do Rust_primitives.Hax.Tuple0.mk));
-  let (_ : Rust_primitives.Hax.Tuple0) ← (pure
+  let _ ← (pure (Lean_tests.Structs.T2._0 (Lean_tests.Structs.T3p._1 t3p)));
+  let _ ← (pure (Lean_tests.Structs.T2._1 (Lean_tests.Structs.T3p._1 t3p)));
+  let _ ← (pure (match t0 with | ⟨⟩ => do Rust_primitives.Hax.Tuple0.mk));
+  let _ ← (pure (match t1 with | ⟨u1⟩ => do Rust_primitives.Hax.Tuple0.mk));
+  let _ ← (pure (match t2 with | ⟨u2, u3⟩ => do Rust_primitives.Hax.Tuple0.mk));
+  let _ ← (pure
+    (match t3 with | ⟨⟨⟩, ⟨u1⟩, ⟨u2, u3⟩⟩ => do Rust_primitives.Hax.Tuple0.mk));
+  let _ ← (pure
     (match t3p with
-      | ⟨(⟨⟩ : Lean_tests.Structs.T0),
-         (⟨(⟨(u1 : i32)⟩ : (Lean_tests.Structs.T1 i32)),
-           (⟨(u2 : i32), (u3 : i32)⟩ : (Lean_tests.Structs.T2 i32 i32))⟩ :
-         (Lean_tests.Structs.T2
-           (Lean_tests.Structs.T1 i32)
-           (Lean_tests.Structs.T2 i32 i32)))⟩
-        => do Rust_primitives.Hax.Tuple0.mk));
+      | ⟨⟨⟩, ⟨⟨u1⟩, ⟨u2, u3⟩⟩⟩ => do Rust_primitives.Hax.Tuple0.mk));
   Rust_primitives.Hax.Tuple0.mk
 
 structure Lean_tests.Structs.S1 where
@@ -419,33 +381,19 @@ def Lean_tests.Structs.normal_structs
       (_theorem := (0 : usize))
       (_structure := (0 : usize))
       (_inductive := (0 : usize))));
-  let ({f1 := (f1 : usize), f2 := (f2 : usize)} : Lean_tests.Structs.S1) ← (pure
-    s1);
-  let
-    ({f1 := (f1 : usize), f2 := (other_name_for_f2 : usize)} :
-    Lean_tests.Structs.S1) ← (pure s1);
-  let
-    ({f1 := ({f1 := (f1 : usize), f2 := (f2 : usize)} : Lean_tests.Structs.S1),
-      f2 := (other_name_for_f2 : usize)} : Lean_tests.Structs.S2) ← (pure s2);
+  let {f1 := f1, f2 := f2} ← (pure s1);
+  let {f1 := f1, f2 := other_name_for_f2} ← (pure s1);
+  let {f1 := {f1 := f1, f2 := f2}, f2 := other_name_for_f2} ← (pure s2);
   let
-    ({_end := (_end : usize),
-      _def := (_def : usize),
-      _theorem := (_theorem : usize),
-      _structure := (_structure : usize),
-      _inductive := (_inductive : usize)} : Lean_tests.Structs.S3) ← (pure s3);
-  let (_ : (Rust_primitives.Hax.Tuple2 usize usize)) ← (pure
+    {_end := _end,
+     _def := _def,
+     _theorem := _theorem,
+     _structure := _structure,
+     _inductive := _inductive} ← (pure s3);
+  let _ ← (pure
     (Rust_primitives.Hax.Tuple2.mk
       (Lean_tests.Structs.S1.f1 s1) (Lean_tests.Structs.S1.f2 s1)));
-  let
-    (_ : (Rust_primitives.Hax.Tuple8
-      usize
-      usize
-      usize
-      usize
-      usize
-      usize
-      usize
-      usize)) ← (pure
+  let _ ← (pure
     (Rust_primitives.Hax.Tuple8.mk
       (Lean_tests.Structs.S1.f1 s1)
       (Lean_tests.Structs.S1.f2 s1)
@@ -455,24 +403,92 @@ def Lean_tests.Structs.normal_structs
       (Lean_tests.Structs.S3._end s3)
       (Lean_tests.Structs.S3._def s3)
       (Lean_tests.Structs.S3._theorem s3)));
-  let (_ : Rust_primitives.Hax.Tuple0) ← (pure
-    (match s1 with
-      | {f1 := (f1 : usize), f2 := (f2 : usize)}
-        => do Rust_primitives.Hax.Tuple0.mk));
-  let (_ : Rust_primitives.Hax.Tuple0) ← (pure
+  let _ ← (pure
+    (match s1 with | {f1 := f1, f2 := f2} => do Rust_primitives.Hax.Tuple0.mk));
+  let _ ← (pure
     (match s2 with
-      | {f1 := ({f1 := (f1 : usize), f2 := (other_name_for_f2 : usize)} :
-         Lean_tests.Structs.S1),
-         f2 := (f2 : usize)}
+      | {f1 := {f1 := f1, f2 := other_name_for_f2}, f2 := f2}
         => do Rust_primitives.Hax.Tuple0.mk));
   (match s3 with
-    | {_end := (_end : usize),
-       _def := (_def : usize),
-       _theorem := (_theorem : usize),
-       _structure := (_structure : usize),
-       _inductive := (_inductive : usize)}
+    | {_end := _end,
+       _def := _def,
+       _theorem := _theorem,
+       _structure := _structure,
+       _inductive := _inductive}
       => do Rust_primitives.Hax.Tuple0.mk)
 
+inductive Lean_tests.Loops.Errors.Error : Type
+| Foo : Lean_tests.Loops.Errors.Error 
+| Bar : u32 -> Lean_tests.Loops.Errors.Error 
+
+
+def Lean_tests.Loops.Errors.loop3
+  (_ : Rust_primitives.Hax.Tuple0)
+  : Result (Core.Result.Result u32 Lean_tests.Loops.Errors.Error)
+  := do
+  let x : u32 ← (pure (0 : u32));
+  (match
+    (← Rust_primitives.Hax.Folds.fold_range_return
+        (1 : i32)
+        (10 : i32)
+        (fun x _ => (do true : Result Bool))
+        x
+        (fun x i => (do
+            (← if (← Rust_primitives.Hax.Machine_int.eq i (5 : i32)) then do
+              (Core.Ops.Control_flow.ControlFlow.Break
+                (Core.Ops.Control_flow.ControlFlow.Break
+                  (Core.Result.Result.Err Lean_tests.Loops.Errors.Error.Foo)))
+            else do
+              (Core.Ops.Control_flow.ControlFlow.Continue (← x +? (5 : u32)))) :
+            Result
+            (Core.Ops.Control_flow.ControlFlow
+              (Core.Ops.Control_flow.ControlFlow
+                (Core.Result.Result u32 Lean_tests.Loops.Errors.Error)
+                (Rust_primitives.Hax.Tuple2 Rust_primitives.Hax.Tuple0 u32))
+              u32))))
+  with
+    | (Core.Ops.Control_flow.ControlFlow.Break ret) => do ret
+    | (Core.Ops.Control_flow.ControlFlow.Continue x)
+      => do (Core.Result.Result.Ok x))
+
+def Lean_tests.Loops.Errors.loop4
+  (_ : Rust_primitives.Hax.Tuple0)
+  : Result
+  (Core.Result.Result
+    (Rust_primitives.Hax.Tuple2 u32 u32)
+    Lean_tests.Loops.Errors.Error)
+  := do
+  let e : u32 ← (pure (0 : u32));
+  let f : Rust_primitives.Hax.Tuple0 -> Result u32 ← (pure
+    (fun ⟨⟩ => (do (42 : u32) : Result u32)));
+  (match
+    (← Rust_primitives.Hax.Folds.fold_range_return
+        (0 : u32)
+        (← Core.Ops.Function.Fn.call
+            f
+            (Rust_primitives.Hax.Tuple1.mk Rust_primitives.Hax.Tuple0.mk))
+        (fun e _ => (do true : Result Bool))
+        e
+        (fun e i => (do
+            (← if (← Rust_primitives.Hax.Machine_int.gt i (10 : u32)) then do
+              (Core.Ops.Control_flow.ControlFlow.Break
+                (Core.Ops.Control_flow.ControlFlow.Break
+                  (Core.Result.Result.Err
+                    (Lean_tests.Loops.Errors.Error.Bar e))))
+            else do
+              (Core.Ops.Control_flow.ControlFlow.Continue (← e +? i))) : Result
+            (Core.Ops.Control_flow.ControlFlow
+              (Core.Ops.Control_flow.ControlFlow
+                (Core.Result.Result
+                  (Rust_primitives.Hax.Tuple2 u32 u32)
+                  Lean_tests.Loops.Errors.Error)
+                (Rust_primitives.Hax.Tuple2 Rust_primitives.Hax.Tuple0 u32))
+              u32))))
+  with
+    | (Core.Ops.Control_flow.ControlFlow.Break ret) => do ret
+    | (Core.Ops.Control_flow.ControlFlow.Continue e)
+      => do (Core.Result.Result.Ok (Rust_primitives.Hax.Tuple2.mk e e)))
+
 inductive Lean_tests.Enums.E : Type
 | V1 : Lean_tests.Enums.E 
 | V2 : Lean_tests.Enums.E 
@@ -502,8 +518,7 @@ def Lean_tests.Enums.enums
     (Lean_tests.Enums.E.V5 (f1 := (23 : usize)) (f2 := (43 : usize))));
   let e_v6 : Lean_tests.Enums.E ← (pure
     (Lean_tests.Enums.E.V6 (f1 := (12 : usize)) (f2 := (13 : usize))));
-  let (nil : (Lean_tests.Enums.MyList usize)) ← (pure
-    Lean_tests.Enums.MyList.Nil);
+  let nil ← (pure Lean_tests.Enums.MyList.Nil);
   let cons_1 : (Lean_tests.Enums.MyList usize) ← (pure
     (Lean_tests.Enums.MyList.Cons (hd := (1 : usize)) (tl := nil)));
   let cons_2_1 : (Lean_tests.Enums.MyList usize) ← (pure
@@ -511,17 +526,16 @@ def Lean_tests.Enums.enums
   (match e_v1 with
     | (Lean_tests.Enums.E.V1 ) => do Rust_primitives.Hax.Tuple0.mk
     | (Lean_tests.Enums.E.V2 ) => do Rust_primitives.Hax.Tuple0.mk
-    | (Lean_tests.Enums.E.V3 (_ : usize)) => do Rust_primitives.Hax.Tuple0.mk
-    | (Lean_tests.Enums.E.V4 (x1 : usize) (x2 : usize) (x3 : usize))
+    | (Lean_tests.Enums.E.V3 _) => do Rust_primitives.Hax.Tuple0.mk
+    | (Lean_tests.Enums.E.V4 x1 x2 x3)
       => do
         let y1 : usize ← (pure (← x1 +? x2));
         let y2 : usize ← (pure (← y1 -? x2));
         let y3 : usize ← (pure (← y2 +? x3));
         Rust_primitives.Hax.Tuple0.mk
-    | (Lean_tests.Enums.E.V5 (f1 := (f1 : usize)) (f2 := (f2 : usize)))
+    | (Lean_tests.Enums.E.V5 (f1 := f1) (f2 := f2))
       => do Rust_primitives.Hax.Tuple0.mk
-    | (Lean_tests.Enums.E.V6
-        (f1 := (f1 : usize)) (f2 := (other_name_for_f2 : usize)))
+    | (Lean_tests.Enums.E.V6 (f1 := f1) (f2 := other_name_for_f2))
       => do Rust_primitives.Hax.Tuple0.mk)
 
 def Lean_tests.FORTYTWO : usize := 42
@@ -543,10 +557,9 @@ def Lean_tests.letBinding (x : usize) (y : usize) : Result usize := do
 
 def Lean_tests.closure (_ : Rust_primitives.Hax.Tuple0) : Result i32 := do
   let x : i32 ← (pure (41 : i32));
-  let f1 : i32 -> Result i32 ← (pure
-    (fun (y : i32) => (do (← y +? x) : Result i32)));
+  let f1 : i32 -> Result i32 ← (pure (fun y => (do (← y +? x) : Result i32)));
   let f2 : i32 -> i32 -> Result i32 ← (pure
-    (fun (y : i32) (z : i32) => (do (← (← y +? x) +? z) : Result i32)));
+    (fun y z => (do (← (← y +? x) +? z) : Result i32)));
   let res1 : i32 ← (pure
     (← Core.Ops.Function.Fn.call f1 (Rust_primitives.Hax.Tuple1.mk (1 : i32))));
   let res2 : i32 ← (pure
@@ -574,4 +587,58 @@ def Lean_tests.binop_resugarings (x : u32) : Result u32 := do
   let rem : u32 ← (pure (← mul %? (4 : u32)));
   let div : u32 ← (pure (← rem /? (5 : u32)));
   let rshift : u32 ← (pure (← div >>>? x));
-  x'''
+  x
+
+def Lean_tests.Loops.loop1 (_ : Rust_primitives.Hax.Tuple0) : Result u32 := do
+  let x ← (pure (0 : u32));
+  let x : u32 ← (pure
+    (← Rust_primitives.Hax.Folds.fold_range
+        (1 : u32)
+        (10 : u32)
+        (fun x _ => (do true : Result Bool))
+        x
+        (fun x i => (do (← x +? i) : Result u32))));
+  x
+
+def Lean_tests.Loops.loop2 (_ : Rust_primitives.Hax.Tuple0) : Result u32 := do
+  let x ← (pure (0 : u32));
+  (match
+    (← Rust_primitives.Hax.Folds.fold_range_return
+        (1 : u32)
+        (10 : u32)
+        (fun x _ => (do true : Result Bool))
+        x
+        (fun x i => (do
+            (← if (← Rust_primitives.Hax.Machine_int.eq i (5 : u32)) then do
+              (Core.Ops.Control_flow.ControlFlow.Break
+                (Core.Ops.Control_flow.ControlFlow.Break x))
+            else do
+              (Core.Ops.Control_flow.ControlFlow.Continue (← x +? i))) : Result
+            (Core.Ops.Control_flow.ControlFlow
+              (Core.Ops.Control_flow.ControlFlow
+                u32
+                (Rust_primitives.Hax.Tuple2 Rust_primitives.Hax.Tuple0 u32))
+              u32))))
+  with
+    | (Core.Ops.Control_flow.ControlFlow.Break ret) => do ret
+    | (Core.Ops.Control_flow.ControlFlow.Continue x) => do x)
+
+def Lean_tests.Ite.test1 (_ : Rust_primitives.Hax.Tuple0) : Result i32 := do
+  let x : i32 ← (pure (← if true then do (0 : i32) else do (1 : i32)));
+  (← if false then do (2 : i32) else do (3 : i32))
+
+def Lean_tests.Ite.test2 (b : Bool) : Result i32 := do
+  let x : i32 ← (pure
+    (← (1 : i32) +? (← if true then do (0 : i32) else do (1 : i32))));
+  let y : i32 ← (pure (0 : i32));
+  let y : i32 ← (pure
+    (← if true then do
+      (← (← y +? x) +? (1 : i32))
+    else do
+      (← (← y -? x) -? (1 : i32))));
+  (← if b then do
+    let z : i32 ← (pure (← y +? y));
+    (← (← z +? y) +? x)
+  else do
+    let z : i32 ← (pure (← y -? x));
+    (← (← z +? y) +? x))'''
diff --git a/tests/lean-tests/src/ite.rs b/tests/lean-tests/src/ite.rs
new file mode 100644
index 000000000..30b8f751d
--- /dev/null
+++ b/tests/lean-tests/src/ite.rs
@@ -0,0 +1,25 @@
+//! Tests on if-then-else
+#![allow(dead_code)]
+#![allow(unused_variables)]
+
+fn test1() -> i32 {
+    let x = if true { 0 } else { 1 };
+    if false { 2 } else { 3 }
+}
+
+fn test2(b: bool) -> i32 {
+    let x = 1 + (if true { 0 } else { 1 });
+    let mut y = 0;
+    if true {
+        y = y + x + 1
+    } else {
+        y = y - x - 1
+    };
+    if b {
+        let z = y + y;
+        z + y + x
+    } else {
+        let z = y - x;
+        z + y + x
+    }
+}
diff --git a/tests/lean-tests/src/lib.rs b/tests/lean-tests/src/lib.rs
index 5dd030221..339886930 100644
--- a/tests/lean-tests/src/lib.rs
+++ b/tests/lean-tests/src/lib.rs
@@ -2,6 +2,8 @@
 #![allow(unused_variables)]
 
 pub mod enums;
+pub mod ite;
+pub mod loops;
 pub mod structs;
 pub mod traits;
 
diff --git a/tests/lean-tests/src/loops.rs b/tests/lean-tests/src/loops.rs
new file mode 100644
index 000000000..d8df81012
--- /dev/null
+++ b/tests/lean-tests/src/loops.rs
@@ -0,0 +1,57 @@
+//! Tests on loops
+#![allow(dead_code)]
+#![allow(unused_variables)]
+
+// Simple loop
+fn loop1() -> u32 {
+    let mut x: u32 = 0;
+    for i in 1..10 {
+        x = x + i
+    }
+    x
+}
+
+// Loop with a return
+fn loop2() -> u32 {
+    let mut x: u32 = 0;
+    for i in 1..10 {
+        if i == 5 {
+            return x;
+        }
+        x = x + i;
+    }
+    x
+}
+
+mod errors {
+    enum Error {
+        Foo,
+        Bar(u32),
+    }
+
+    fn loop3() -> Result<u32, Error> {
+        let mut x = 0;
+        for i in 1..10 {
+            if i == 5 {
+                return Err(Error::Foo);
+            }
+            x = x + 5
+        }
+        Ok(x)
+    }
+
+    fn loop4() -> Result<(u32, u32), Error> {
+        let mut e = 0;
+        let f = |()| 42;
+
+        for i in 0..(f(())) {
+            // verify degree bound
+            if i > 10 {
+                return Err(Error::Bar(e));
+            }
+            e = e + i
+        }
+
+        Ok((e, e))
+    }
+}