fix formatting

anoma · Oct 28, 2024 · 1143b67 · 1143b67
1 parent da9c11c
commit 1143b67
Show file tree

Hide file tree

Showing 8 changed files with 19 additions and 19 deletions.
diff --git a/examples/demo/Demo.juvix b/examples/demo/Demo.juvix
@@ -22,7 +22,7 @@ type Tree (A : Type) :=
   | node@{
       element : A;
       left : Tree A;
-      right : Tree A
+      right : Tree A;
     };
 
 mirror {A} : (tree : Tree A) -> Tree A

diff --git a/examples/milestone/Bank/Bank.juvix b/examples/milestone/Bank/Bank.juvix
@@ -17,7 +17,7 @@ type Token :=
   mkToken@{
     owner : Address;
     gates : Nat;
-    amount : Nat
+    amount : Nat;
   };
 
 --- This module defines the type for balances and its associated operations.

diff --git a/examples/milestone/Hanoi/Hanoi.juvix b/examples/milestone/Hanoi/Hanoi.juvix
@@ -43,7 +43,7 @@ showPeg : Peg -> String
 type Move :=
   mkMove@{
     from : Peg;
-    to : Peg
+    to : Peg;
   };
 
 showMove (move : Move) : String :=

diff --git a/examples/milestone/TicTacToe/Logic/Game.juvix b/examples/milestone/TicTacToe/Logic/Game.juvix
@@ -38,7 +38,7 @@ playMove (attemptedMove : Maybe Nat) (state : GameState) : GameState :=
             mkGameState@{
               board := mkBoard (map (map (replace player' k)) squares);
               player := switch player';
-              error := noError
+              error := noError;
             };
 
 --- Returns ;just; if the given ;Nat; is in range of 1..9

diff --git a/examples/milestone/TicTacToe/Logic/GameState.juvix b/examples/milestone/TicTacToe/Logic/GameState.juvix
@@ -16,7 +16,7 @@ type GameState :=
   mkGameState@{
     board : Board;
     player : Symbol;
-    error : Error
+    error : Error;
   };
 
 --- Textual representation of a ;GameState;
@@ -34,7 +34,7 @@ beginState : GameState :=
             :: (7 :: 8 :: 9 :: nil)
             :: nil));
     player := X;
-    error := noError
+    error := noError;
   };
 
 --- ;true; if some player has won the game

diff --git a/examples/milestone/TicTacToe/Logic/Square.juvix b/examples/milestone/TicTacToe/Logic/Square.juvix
@@ -18,7 +18,7 @@ eqSquareI : Eq Square :=
       case square1, square2 of
         | empty m, empty n := m == n
         | occupied s, occupied t := s == t
-        | _, _ := false
+        | _, _ := false;
   };
 
 --- Textual representation of a ;Square;

diff --git a/examples/milestone/TicTacToe/Logic/Symbol.juvix b/examples/milestone/TicTacToe/Logic/Symbol.juvix
@@ -17,7 +17,7 @@ eqSymbolI : Eq Symbol :=
       case sym1, sym2 of
         | O, O := true
         | X, X := true
-        | _, _ := false
+        | _, _ := false;
   };
 
 --- Turns ;O; into ;X; and ;X; into ;O;

diff --git a/tests/positive/Isabelle/Program.juvix b/tests/positive/Isabelle/Program.juvix
@@ -113,13 +113,13 @@ type Either' A B :=
 type R' :=
   mkR'@{
     r1' : Nat;
-    r2' : Nat
+    r2' : Nat;
   };
 
 type R :=
   mkR@{
     r1 : Nat;
-    r2 : Nat
+    r2 : Nat;
   };
 
 r : R := mkR 0 1;
@@ -135,52 +135,52 @@ funR' : R -> R
   | mkR@{r1 := rr1; r2 := rr2} :=
     mkR@{
       r1 := rr1 + rr2;
-      r2 := rr2
+      r2 := rr2;
     };
 
 funR1 : R -> R
   | mkR@{r1 := zero; r2} :=
     mkR@{
       r1 := r2;
-      r2
+      r2;
     }
   | mkR@{r1 := rr1; r2 := rr2} :=
     mkR@{
       r1 := rr2;
-      r2 := rr1
+      r2 := rr1;
     };
 
 funR2 (r : R) : R :=
   case r of
     | mkR@{r1 := zero; r2} :=
       mkR@{
         r1 := r2;
-        r2
+        r2;
       }
     | mkR@{r1 := rr1; r2 := rr2} :=
       mkR@{
         r1 := rr2;
-        r2 := rr1
+        r2 := rr1;
       };
 
 funR3 (er : Either' R R) : R :=
   case er of
     | Left' mkR@{r1 := zero; r2} :=
       mkR@{
         r1 := r2;
-        r2
+        r2;
       }
     | Left' mkR@{r1 := rr1; r2 := rr2} :=
       mkR@{
         r1 := rr2;
-        r2 := rr1
+        r2 := rr1;
       }
     | Right' mkR@{r1; r2 := zero} :=
       mkR@{
         r1 := 7;
-        r2 := r1
+        r2 := r1;
       }
-    | Right' r@mkR@{r1; r2} := r@R{   r1 := r2 + 2; r2 := r1 + 3 };
+    | Right' r@mkR@{r1; r2} := r@R{r1 := r2 + 2; r2 := r1 + 3};
 
 funR4 : R -> R
   | r@mkR@{r1} := r@R{r2 := r1};