Make sure let-bindings in Lean end with line breaks and improve formatting

1 files changed, 7 insertions, 2 deletions

diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index e13743c4..40005671 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -152,8 +152,8 @@ let fun_sig_substitute (tsubst : TypeVarId.id -> ty) (sg : fun_sig) :
     We only look for outer monadic let-bindings.
     This is used when printing the branches of [if ... then ... else ...].
 
-    Rem.: this function will *fail* if there are {!constructor:Aeneas.Pure.expression.Loop} nodes (you should call
-    it on an expression where those nodes have been eliminated).
+    Rem.: this function will *fail* if there are {!constructor:Aeneas.Pure.expression.Loop}
+    nodes (you should call it on an expression where those nodes have been eliminated).
  *)
 let rec let_group_requires_parentheses (e : texpression) : bool =
   match e.e with
@@ -166,6 +166,11 @@ let rec let_group_requires_parentheses (e : texpression) : bool =
       (* Should have been eliminated *)
       raise (Failure "Unreachable")
 
+let texpression_requires_parentheses e =
+  match !Config.backend with
+  | FStar | Lean -> false
+  | Coq -> let_group_requires_parentheses e
+
 let is_var (e : texpression) : bool =
   match e.e with Var _ -> true | _ -> false