format

examples/milestone/Collatz/Collatz.juvix

@@ -25,4 +25,4 @@ resultHeading : String := "Collatz sequence:";
 
 main : IO :=
   printStringLn welcome
-    >>> readLn λ {s := printStringLn resultHeading >>> run collatz (stringToNat s)};
+    >>> readLn λ{s := printStringLn resultHeading >>> run collatz (stringToNat s)};

tests/positive/Format.juvix

@@ -167,7 +167,7 @@ exampleFunction2
     -> List A
     -> List A
     -> Nat :=
-  λ {_ _ _ _ _ _ _ _ _ _ :=
+  λ{_ _ _ _ _ _ _ _ _ _ :=
     undefined
       -- comment after first
       + undefined
@@ -186,11 +186,11 @@ positive
 type T0 (A : Type) := c0 : (A -> T0 A) -> T0 A;
 
 -- Single Lambda clause
-idLambda : {A : Type} -> A -> A := λ {x := x};
+idLambda : {A : Type} -> A -> A := λ{x := x};
 
 -- Lambda clauses
 f : Nat -> Nat :=
-  \ {
+  \{
     -- comment before lambda pipe
     | zero :=
       let
@@ -305,7 +305,7 @@ module Traits;
   instance
   showBoolI : Show Bool :=
     mkShow@{
-      show := λ {x := ite x "true" "false"}
+      show := λ{x := ite x "true" "false"}
     };
 
   instance

tests/positive/InstanceImport/M.juvix

@@ -6,4 +6,4 @@ type T A := mkT@{pp : A → A};
 type Unit := unit;
 
 instance
-unitI : T Unit := mkT λ {x := x};
+unitI : T Unit := mkT λ{x := x};

tests/positive/InstanceImport/Main.juvix

@@ -8,6 +8,6 @@ type Bool :=
   | false;
 
 instance
-boolI : T Bool := mkT λ {x := x};
+boolI : T Bool := mkT λ{x := x};
 
 main : Bool := case T.pp unit of unit := T.pp true;

tests/positive/SignatureWithBody.juvix

@@ -3,15 +3,15 @@ module SignatureWithBody;
 import Stdlib.Prelude open;
 
 isNull : {A : Type} → List A → Bool :=
-  λ {
+  λ{
     | nil := true
     | _ := false
   };
 
 isNull' : {A : Type} → List A → Bool :=
   let
     aux : {A : Type} → List A → Bool :=
-      λ {
+      λ{
         | nil := true
         | _ := false
       };

tests/positive/StdlibList/Data/List.juvix

@@ -27,7 +27,7 @@ filter : (a : Type) → (a → Bool) → List a → List a
   | a f (:: h hs) :=
     match
       (f h)
-      λ {
+      λ{
         | true := :: h (filter a f hs)
         | false := filter a f hs
       };
@@ -65,14 +65,14 @@ splitAt : (a : Type) → ℕ → List a → List a × List a
   | a _ nil := , nil nil
   | a zero xs := , nil xs
   | a (suc zero) (:: x xs) := , (:: x nil) xs
-  | a (suc (suc m)) (:: x xs) := match (splitAt a m xs) λ {(, xs' xs'') := , (:: x xs') xs''};
+  | a (suc (suc m)) (:: x xs) := match (splitAt a m xs) λ{(, xs' xs'') := , (:: x xs') xs''};
 
 terminating
 merge : (a : Type) → (a → a → Ordering) → List a → List a → List a
   | a cmp (:: x xs) (:: y ys) :=
     match
       (cmp x y)
-      λ {
+      λ{
         | LT := :: x (merge a cmp xs (:: y ys))
         | _ := :: y (merge a cmp (:: x xs) ys)
       }
@@ -92,7 +92,7 @@ quickSort : (a : Type) → (a → a → Ordering) → List a → List a
       ltx (y : a) : Bool :=
         match
           (cmp y x)
-          λ {
+          λ{
             | LT := true
             | _ := false
           };