run make format-juvix-files

examples/milestone/Bank/Bank.juvix

@@ -100,8 +100,8 @@ issue : Address -> Address -> Nat -> Token
     assert (caller == bankAddress) (mkToken owner 0 amount);
 
 --- Deposits some amount of money into the bank.
-deposit (bal : Balances) (token : Token) (amount : Nat)
-  : Token :=
+deposit
+  (bal : Balances) (token : Token) (amount : Nat) : Token :=
   let
     difference : Nat := sub (getAmount token) amount;
     remaining : Token :=
@@ -111,7 +111,13 @@ deposit (bal : Balances) (token : Token) (amount : Nat)
   in runOnChain (commitBalances bal') remaining;
 
 --- Returns a new ;Token; containing the amount of money withdrawn.
-withdraw (bal : Balances) (caller : Address) (recipient : Address) (amount : Nat) (rate : Nat) (periods : Nat)
+withdraw
+  (bal : Balances)
+  (caller : Address)
+  (recipient : Address)
+  (amount : Nat)
+  (rate : Nat)
+  (periods : Nat)
   : Token :=
   assert
     (caller == bankAddress)

tests/negative/Internal/DefaultArgCycleArity.juvix

@@ -2,6 +2,8 @@ module DefaultArgCycleArity;
 
 import Stdlib.Data.Nat open;
 
-fun {a : Nat := 1} {b : Nat := fun + a + 1} {c : Nat := b
-  + a
-  + 1} : Nat := a * b + c;
+fun
+  {a : Nat := 1}
+  {b : Nat := fun + a + 1}
+  {c : Nat := b + a + 1}
+  : Nat := a * b + c;

tests/positive/ConstructorWildcard.juvix

@@ -1,16 +1,17 @@
 module ConstructorWildcard;
 
 type Bool :=
- false | true;
+  | false
+  | true;
 
 type either (A B : Type) :=
-  left A
+  | left A
   | right B;
 
 isLeft {A B} : either A B → Bool
- | left@{} := true
- | right@{} := false;
+  | left@{} := true
+  | right@{} := false;
 
 not : Bool → Bool
- | false@{} := true
- | true := false;
+  | false@{} := true
+  | true := false;

tests/positive/DefaultValues.juvix

@@ -18,12 +18,22 @@ axiom c : C;
 
 axiom d : D;
 
-mk {f1 : A := a} {f2 : Type} {f3 : C := c} (x : f2)
+mk
+  {f1 : A := a}
+  {f2 : Type}
+  {f3 : C := c}
+  (x : f2)
   : A × f2 × C := f1, x, f3;
 
 x1 : A × B × C := mk (x := b);
 
-mk2 {f1 : A := a} {f2 : Type} {f3 : C := c} (x : f2) {f4 : D := d} (y : f2)
+mk2
+  {f1 : A := a}
+  {f2 : Type}
+  {f3 : C := c}
+  (x : f2)
+  {f4 : D := d}
+  (y : f2)
   : A × f2 × C := f1, x, f3;
 
 x2 : A × B × C := mk2 (x := b) (y := b);

tests/positive/Traits2.juvix

@@ -51,8 +51,8 @@ syntax operator >>= bind;
     -> (A -> M B)
     -> M B := Monad.bind;
 
-Maybe-bind {A B : Type}
-  : Maybe A -> (A -> Maybe B) -> Maybe B
+Maybe-bind
+  {A B : Type} : Maybe A -> (A -> Maybe B) -> Maybe B
   | nothing _ := nothing
   | (just a) f := f a;
 
@@ -74,13 +74,16 @@ import Stdlib.Data.Product open;
 ×-Functor : {A : Type} -> Functor ((×) A) :=
   mkFunctor ×-fmap;
 
-×-bind {A : Type} {{Semigroup A}} {B C : Type}
+×-bind
+  {A : Type}
+  {{Semigroup A}}
+  {B C : Type}
   : A × B -> (B -> A × C) -> A × C
   | (a, b) f := case f b of {a', b' := a <> a', b'};
 
 instance
-×-Monad {A : Type} {{Semigroup A}} {{Monoid A}}
-  : Monad ((×) A) :=
+×-Monad
+  {A : Type} {{Semigroup A}} {{Monoid A}} : Monad ((×) A) :=
   mkMonad@{
     bind := ×-bind;
     return := λ {b := Monoid.mempty, b};
@@ -89,8 +92,8 @@ instance
 
 type Reader (r a : Type) := mkReader {runReader : r -> a};
 
-Reader-fmap {R A B : Type} (f : A -> B)
-  : Reader R A -> Reader R B
+Reader-fmap
+  {R A B : Type} (f : A -> B) : Reader R A -> Reader R B
   | (mkReader ra) := mkReader (f ∘ ra);
 
 Reader-Functor-NoNamed {R : Type} : Functor (Reader R) :=
@@ -109,7 +112,8 @@ Reader-Monad {R : Type} : Monad (Reader R) :=
     functor := Reader-Functor;
     return {A : Type} (a : A) : Reader R A :=
       mkReader (const a);
-    bind {A B : Type}
+    bind
+      {A B : Type}
       : Reader R A -> (A -> Reader R B) -> Reader R B
       | (mkReader ra) arb :=
         let