Format juvix files using new function syntax (#2245)

examples/demo/Demo.juvix

@@ -6,51 +6,49 @@ import Stdlib.Prelude open;
 import Stdlib.Data.Nat.Ord open;
 -- for Ordering
 
-even : Nat → Bool;
-even zero := true;
-even (suc zero) := false;
-even (suc (suc n)) := even n;
+even : Nat → Bool
+  | zero := true
+  | (suc zero) := false
+  | (suc (suc n)) := even n;
 
-even' : Nat → Bool;
-even' n := mod n 2 == 0;
+even' : Nat → Bool
+  | n := mod n 2 == 0;
 
 -- base 2 logarithm rounded down
 terminating
-log2 : Nat → Nat;
-log2 n := if (n <= 1) 0 (suc (log2 (div n 2)));
+log2 : Nat → Nat
+  | n := if (n <= 1) 0 (suc (log2 (div n 2)));
 
 type Tree (A : Type) :=
   | leaf : A → Tree A
   | node : A → Tree A → Tree A → Tree A;
 
-mirror : {A : Type} → Tree A → Tree A;
-mirror t@(leaf _) := t;
-mirror (node x l r) := node x (mirror r) (mirror l);
+mirror : {A : Type} → Tree A → Tree A
+  | t@(leaf _) := t
+  | (node x l r) := node x (mirror r) (mirror l);
 
-tree : Tree Nat;
-tree := node 2 (node 3 (leaf 0) (leaf 1)) (leaf 7);
+tree : Tree Nat :=
+  node 2 (node 3 (leaf 0) (leaf 1)) (leaf 7);
 
-preorder : {A : Type} → Tree A → List A;
-preorder (leaf x) := x :: nil;
-preorder (node x l r) :=
-  x :: nil ++ preorder l ++ preorder r;
+preorder : {A : Type} → Tree A → List A
+  | (leaf x) := x :: nil
+  | (node x l r) := x :: nil ++ preorder l ++ preorder r;
 
 terminating
-sort : {A : Type} → (A → A → Ordering) → List A → List A;
-sort _ nil := nil;
-sort _ xs@(_ :: nil) := xs;
-sort {A} cmp xs :=
-  uncurry
-    (merge (mkOrd cmp))
-    (both (sort cmp) (splitAt (div (length xs) 2) xs));
+sort : {A : Type} → (A → A → Ordering) → List A → List A
+  | _ nil := nil
+  | _ xs@(_ :: nil) := xs
+  | {A} cmp xs :=
+    uncurry
+      (merge (mkOrd cmp))
+      (both (sort cmp) (splitAt (div (length xs) 2) xs));
 
-printNatListLn : List Nat → IO;
-printNatListLn nil := printStringLn "nil";
-printNatListLn (x :: xs) :=
-  printNat x >> printString " :: " >> printNatListLn xs;
+printNatListLn : List Nat → IO
+  | nil := printStringLn "nil"
+  | (x :: xs) :=
+    printNat x >> printString " :: " >> printNatListLn xs;
 
-main : IO;
-main :=
+main : IO :=
   printStringLn "Hello!"
     >> printNatListLn (preorder (mirror tree))
     >> printNatListLn (sort compare (preorder (mirror tree)))

examples/midsquare/MidSquareHash.juvix

@@ -8,22 +8,21 @@ import Stdlib.Prelude open;
 import Stdlib.Data.Nat.Ord open;
 
 --- `pow N` is 2 ^ N
-pow : Nat -> Nat;
-pow zero := 1;
-pow (suc n) := 2 * pow n;
+pow : Nat -> Nat
+  | zero := 1
+  | (suc n) := 2 * pow n;
 
 --- `hash' N` hashes a number with max N bits (i.e. smaller than 2^N) into 6 bits
 --- (i.e. smaller than 64) using the mid-square algorithm.
-hash' : Nat -> Nat -> Nat;
-hash' (suc n@(suc (suc m))) x :=
-  if
-    (x < pow n)
-    (hash' n x)
-    (mod (div (x * x) (pow m)) (pow 6));
-hash' _ x := x * x;
+hash' : Nat -> Nat -> Nat
+  | (suc n@(suc (suc m))) x :=
+    if
+      (x < pow n)
+      (hash' n x)
+      (mod (div (x * x) (pow m)) (pow 6))
+  | _ x := x * x;
 
 hash : Nat -> Nat := hash' 16;
 
-main : Nat;
-main := hash 1367;
+main : Nat := hash 1367;
 -- result: 3

examples/midsquare/MidSquareHashUnrolled.juvix

@@ -45,72 +45,71 @@ pow16 : Nat := 2 * pow15;
 
 --- `hashN` hashes a number with max N bits (i.e. smaller than 2^N) into 6 bits
 --- (i.e. smaller than 64) using the mid-square algorithm.
-hash0 : Nat -> Nat;
-hash0 x := 0;
+hash0 : Nat -> Nat
+  | x := 0;
 
-hash1 : Nat -> Nat;
-hash1 x := x * x;
+hash1 : Nat -> Nat
+  | x := x * x;
 
-hash2 : Nat -> Nat;
-hash2 x := x * x;
+hash2 : Nat -> Nat
+  | x := x * x;
 
-hash3 : Nat -> Nat;
-hash3 x := x * x;
+hash3 : Nat -> Nat
+  | x := x * x;
 
-hash4 : Nat -> Nat;
-hash4 x :=
-  if (x < pow3) (hash3 x) (mod (div (x * x) pow1) pow6);
+hash4 : Nat -> Nat
+  | x :=
+    if (x < pow3) (hash3 x) (mod (div (x * x) pow1) pow6);
 
-hash5 : Nat -> Nat;
-hash5 x :=
-  if (x < pow4) (hash4 x) (mod (div (x * x) pow2) pow6);
+hash5 : Nat -> Nat
+  | x :=
+    if (x < pow4) (hash4 x) (mod (div (x * x) pow2) pow6);
 
-hash6 : Nat -> Nat;
-hash6 x :=
-  if (x < pow5) (hash5 x) (mod (div (x * x) pow3) pow6);
+hash6 : Nat -> Nat
+  | x :=
+    if (x < pow5) (hash5 x) (mod (div (x * x) pow3) pow6);
 
-hash7 : Nat -> Nat;
-hash7 x :=
-  if (x < pow6) (hash6 x) (mod (div (x * x) pow4) pow6);
+hash7 : Nat -> Nat
+  | x :=
+    if (x < pow6) (hash6 x) (mod (div (x * x) pow4) pow6);
 
-hash8 : Nat -> Nat;
-hash8 x :=
-  if (x < pow7) (hash7 x) (mod (div (x * x) pow5) pow6);
+hash8 : Nat -> Nat
+  | x :=
+    if (x < pow7) (hash7 x) (mod (div (x * x) pow5) pow6);
 
-hash9 : Nat -> Nat;
-hash9 x :=
-  if (x < pow8) (hash8 x) (mod (div (x * x) pow6) pow6);
+hash9 : Nat -> Nat
+  | x :=
+    if (x < pow8) (hash8 x) (mod (div (x * x) pow6) pow6);
 
-hash10 : Nat -> Nat;
-hash10 x :=
-  if (x < pow9) (hash9 x) (mod (div (x * x) pow7) pow6);
+hash10 : Nat -> Nat
+  | x :=
+    if (x < pow9) (hash9 x) (mod (div (x * x) pow7) pow6);
 
-hash11 : Nat -> Nat;
-hash11 x :=
-  if (x < pow10) (hash10 x) (mod (div (x * x) pow8) pow6);
+hash11 : Nat -> Nat
+  | x :=
+    if (x < pow10) (hash10 x) (mod (div (x * x) pow8) pow6);
 
-hash12 : Nat -> Nat;
-hash12 x :=
-  if (x < pow11) (hash11 x) (mod (div (x * x) pow9) pow6);
+hash12 : Nat -> Nat
+  | x :=
+    if (x < pow11) (hash11 x) (mod (div (x * x) pow9) pow6);
 
-hash13 : Nat -> Nat;
-hash13 x :=
-  if (x < pow12) (hash12 x) (mod (div (x * x) pow10) pow6);
+hash13 : Nat -> Nat
+  | x :=
+    if (x < pow12) (hash12 x) (mod (div (x * x) pow10) pow6);
 
-hash14 : Nat -> Nat;
-hash14 x :=
-  if (x < pow13) (hash13 x) (mod (div (x * x) pow11) pow6);
+hash14 : Nat -> Nat
+  | x :=
+    if (x < pow13) (hash13 x) (mod (div (x * x) pow11) pow6);
 
-hash15 : Nat -> Nat;
-hash15 x :=
-  if (x < pow14) (hash14 x) (mod (div (x * x) pow12) pow6);
+hash15 : Nat -> Nat
+  | x :=
+    if (x < pow14) (hash14 x) (mod (div (x * x) pow12) pow6);
 
-hash16 : Nat -> Nat;
-hash16 x :=
-  if (x < pow15) (hash15 x) (mod (div (x * x) pow13) pow6);
+hash16 : Nat -> Nat
+  | x :=
+    if (x < pow15) (hash15 x) (mod (div (x * x) pow13) pow6);
 
 hash : Nat -> Nat := hash16;
 
-main : Nat;
-main := hash 1367;
+main : Nat := hash 1367;
 -- result: 3

examples/milestone/Bank/Bank.juvix

@@ -10,11 +10,9 @@ import Stdlib.Data.Nat.Ord open;
 
 import Stdlib.Data.Nat as Nat;
 
-Address : Type;
-Address := Nat;
+Address : Type := Nat;
 
-bankAddress : Address;
-bankAddress := 1234;
+bankAddress : Address := 1234;
 
 --- Some field type.
 axiom Field : Type;
@@ -28,47 +26,45 @@ module Token;
       mkToken : Address -> Nat -> Nat -> Token;
 
   --- Retrieves the owner from a ;Token;
-  getOwner : Token -> Address;
-  getOwner (mkToken o _ _) := o;
+  getOwner : Token -> Address
+    | (mkToken o _ _) := o;
 
   --- Retrieves the amount from a ;Token;
-  getAmount : Token -> Nat;
-  getAmount (mkToken _ _ a) := a;
+  getAmount : Token -> Nat
+    | (mkToken _ _ a) := a;
 
   --- Retrieves the gates from a ;Token;
-  getGates : Token -> Nat;
-  getGates (mkToken _ g _) := g;
+  getGates : Token -> Nat
+    | (mkToken _ g _) := g;
 end;
 
 open Token;
 
 --- This module defines the type for balances and its associated operations.
 module Balances;
-  Balances : Type;
-  Balances := List (Field × Nat);
+  Balances : Type := List (Field × Nat);
 
   --- Increments the amount associated with a certain ;Field;.
-  increment : Field -> Nat -> Balances -> Balances;
-  increment f n nil := (f, n) :: nil;
-  increment f n ((b, bn) :: bs) :=
-    if
-      (eqField f b)
-      ((b, bn + n) :: bs)
-      ((b, bn) :: increment f n bs);
+  increment : Field -> Nat -> Balances -> Balances
+    | f n nil := (f, n) :: nil
+    | f n ((b, bn) :: bs) :=
+      if
+        (eqField f b)
+        ((b, bn + n) :: bs)
+        ((b, bn) :: increment f n bs);
 
   --- Decrements the amount associated with a certain ;Field;.
   --- If the ;Field; is not found, it does nothing.
   --- Subtraction is truncated to ;zero;.
-  decrement : Field -> Nat -> Balances -> Balances;
-  decrement _ _ nil := nil;
-  decrement f n ((b, bn) :: bs) :=
-    if
-      (eqField f b)
-      ((b, sub bn n) :: bs)
-      ((b, bn) :: decrement f n bs);
+  decrement : Field -> Nat -> Balances -> Balances
+    | _ _ nil := nil
+    | f n ((b, bn) :: bs) :=
+      if
+        (eqField f b)
+        ((b, sub bn n) :: bs)
+        ((b, bn) :: decrement f n bs);
 
-  emtpyBalances : Balances;
-  emtpyBalances := nil;
+  emtpyBalances : Balances := nil;
 
   --- Commit balances changes to the chain.
   axiom commitBalances : Balances -> IO;
@@ -83,17 +79,17 @@ axiom runOnChain : {B : Type} -> IO -> B -> B;
 axiom hashAddress : Address -> Field;
 
 --- Returns the total amount of tokens after compounding interest.
-calculateInterest : Nat -> Nat -> Nat -> Nat;
-calculateInterest principal rate periods :=
-  let
-    amount : Nat := principal;
-    incrAmount : Nat -> Nat;
-    incrAmount a := div (a * rate) 10000;
-  in iterate (min 100 periods) incrAmount amount;
+calculateInterest : Nat -> Nat -> Nat -> Nat
+  | principal rate periods :=
+    let
+      amount : Nat := principal;
+      incrAmount : Nat -> Nat;
+      incrAmount a := div (a * rate) 10000;
+    in iterate (min 100 periods) incrAmount amount;
 
 --- Asserts some ;Bool; condition.
-assert : {A : Type} -> Bool -> A -> A;
-assert c a := if c a (fail "assertion failed");
+assert : {A : Type} -> Bool -> A -> A
+  | c a := if c a (fail "assertion failed");
 
 --- Returns a new ;Token;. Arguments are:
 ---
@@ -102,9 +98,9 @@ assert c a := if c a (fail "assertion failed");
 --- `amount`: The amount of  tokens to issue
 ---
 --- `caller`: Who is creating the transaction. It must be the bank.
-issue : Address -> Address -> Nat -> Token;
-issue caller owner amount :=
-  assert (caller == bankAddress) (mkToken owner 0 amount);
+issue : Address -> Address -> Nat -> Token
+  | caller owner amount :=
+    assert (caller == bankAddress) (mkToken owner 0 amount);
 
 {-
 -- TODO: Uncomment this block once we fix

examples/milestone/Collatz/Collatz.juvix

@@ -3,29 +3,26 @@ module Collatz;
 import Stdlib.Prelude open;
 import Stdlib.Data.Nat.Ord open;
 
-collatzNext : Nat → Nat;
-collatzNext n := if (mod n 2 == 0) (div n 2) (3 * n + 1);
+collatzNext : Nat → Nat
+  | n := if (mod n 2 == 0) (div n 2) (3 * n + 1);
 
-collatz : Nat → Nat;
-collatz zero := zero;
-collatz (suc zero) := suc zero;
-collatz n := collatzNext n;
+collatz : Nat → Nat
+  | zero := zero
+  | (suc zero) := suc zero
+  | n := collatzNext n;
 
 terminating
-run : (Nat → Nat) → Nat → IO;
-run _ (suc zero) :=
-  printNatLn 1 >> printStringLn "Finished!";
-run f n := printNatLn n >> run f (f n);
+run : (Nat → Nat) → Nat → IO
+  | _ (suc zero) :=
+    printNatLn 1 >> printStringLn "Finished!"
+  | f n := printNatLn n >> run f (f n);
 
-welcome : String;
-welcome :=
+welcome : String :=
   "Collatz calculator\n------------------\n\nType a number then ENTER";
 
-resultHeading : String;
-resultHeading := "Collatz sequence:";
+resultHeading : String := "Collatz sequence:";
 
-main : IO;
-main :=
+main : IO :=
   printStringLn welcome
     >> readLn
       λ {s :=

examples/milestone/Fibonacci/Fibonacci.juvix

@@ -2,12 +2,11 @@ module Fibonacci;
 
 import Stdlib.Prelude open;
 
-fib : Nat → Nat → Nat → Nat;
-fib zero x1 _ := x1;
-fib (suc n) x1 x2 := fib n x2 (x1 + x2);
+fib : Nat → Nat → Nat → Nat
+  | zero x1 _ := x1
+  | (suc n) x1 x2 := fib n x2 (x1 + x2);
 
-fibonacci : Nat → Nat;
-fibonacci n := fib n 0 1;
+fibonacci : Nat → Nat
+  | n := fib n 0 1;
 
-main : IO;
-main := readLn (printNatLn ∘ fibonacci ∘ stringToNat);
+main : IO := readLn (printNatLn ∘ fibonacci ∘ stringToNat);

examples/milestone/Hanoi/Hanoi.juvix

@@ -18,20 +18,19 @@ import Stdlib.Prelude open;
 --- ;concat (("a" :: nil) :: "b" :: nil); evaluates to ;"a"
   :: "b"
   :: nil;
-concat : List String → String;
-concat := foldl (++str) "";
+concat : List String → String := foldl (++str) "";
 
-intercalate : String → List String → String;
-intercalate sep xs := concat (intersperse sep xs);
+intercalate : String → List String → String
+  | sep xs := concat (intersperse sep xs);
 
 --- Produce a singleton List
-singleton : {A : Type} → A → List A;
-singleton a := a :: nil;
+singleton : {A : Type} → A → List A
+  | a := a :: nil;
 
 --- Produce a ;String; representation of a ;List Nat;
-showList : List Nat → String;
-showList xs :=
-  "[" ++str intercalate "," (map natToString xs) ++str "]";
+showList : List Nat → String
+  | xs :=
+    "[" ++str intercalate "," (map natToString xs) ++str "]";
 
 --- A Peg represents a peg in the towers of Hanoi game
 type Peg :=
@@ -39,28 +38,27 @@ type Peg :=
   | middle : Peg
   | right : Peg;
 
-showPeg : Peg → String;
-showPeg left := "left";
-showPeg middle := "middle";
-showPeg right := "right";
+showPeg : Peg → String
+  | left := "left"
+  | middle := "middle"
+  | right := "right";
 
 --- A Move represents a move between pegs
 type Move :=
   | move : Peg → Peg → Move;
 
-showMove : Move → String;
-showMove (move from to) :=
-  showPeg from ++str " -> " ++str showPeg to;
+showMove : Move → String
+  | (move from to) :=
+    showPeg from ++str " -> " ++str showPeg to;
 
 --- Produce a list of ;Move;s that solves the towers of Hanoi game
-hanoi : Nat → Peg → Peg → Peg → List Move;
-hanoi zero _ _ _ := nil;
-hanoi (suc n) p1 p2 p3 :=
-  hanoi n p1 p3 p2
-    ++ singleton (move p1 p2)
-    ++ hanoi n p3 p2 p1;
+hanoi : Nat → Peg → Peg → Peg → List Move
+  | zero _ _ _ := nil
+  | (suc n) p1 p2 p3 :=
+    hanoi n p1 p3 p2
+      ++ singleton (move p1 p2)
+      ++ hanoi n p3 p2 p1;
 
-main : IO;
-main :=
+main : IO :=
   printStringLn
     (unlines (map showMove (hanoi 5 left middle right)));

examples/milestone/HelloWorld/HelloWorld.juvix

@@ -3,5 +3,4 @@ module HelloWorld;
 
 import Stdlib.Prelude open;
 
-main : IO;
-main := printStringLn "hello world!";
+main : IO := printStringLn "hello world!";

examples/milestone/PascalsTriangle/PascalsTriangle.juvix

@@ -7,39 +7,38 @@ module PascalsTriangle;
 import Stdlib.Prelude open;
 
 --- Return a list of repeated applications of a given function
-scanIterate : {A : Type} → Nat → (A → A) → A → List A;
-scanIterate zero _ _ := nil;
-scanIterate (suc n) f a := a :: scanIterate n f (f a);
+scanIterate : {A : Type} → Nat → (A → A) → A → List A
+  | zero _ _ := nil
+  | (suc n) f a := a :: scanIterate n f (f a);
 
 --- Produce a singleton List
-singleton : {A : Type} → A → List A;
-singleton a := a :: nil;
+singleton : {A : Type} → A → List A
+  | a := a :: nil;
 
 --- Concatenates a list of strings
 --- ;concat (("a" :: nil) :: "b" :: nil); evaluates to ;"a"
   :: "b"
   :: nil;
-concat : List String → String;
-concat := foldl (++str) "";
+concat : List String → String := foldl (++str) "";
 
-intercalate : String → List String → String;
-intercalate sep xs := concat (intersperse sep xs);
+intercalate : String → List String → String
+  | sep xs := concat (intersperse sep xs);
 
-showList : List Nat → String;
-showList xs :=
-  "[" ++str intercalate "," (map natToString xs) ++str "]";
+showList : List Nat → String
+  | xs :=
+    "[" ++str intercalate "," (map natToString xs) ++str "]";
 
 --- Compute the next row of Pascal's triangle
-pascalNextRow : List Nat → List Nat;
-pascalNextRow row :=
-  zipWith
-    (+)
-    (singleton zero ++ row)
-    (row ++ singleton zero);
+pascalNextRow : List Nat → List Nat
+  | row :=
+    zipWith
+      (+)
+      (singleton zero ++ row)
+      (row ++ singleton zero);
 
 --- Produce Pascal's triangle to a given depth
-pascal : Nat → List (List Nat);
-pascal rows := scanIterate rows pascalNextRow (singleton 1);
+pascal : Nat → List (List Nat)
+  | rows := scanIterate rows pascalNextRow (singleton 1);
 
-main : IO;
-main := printStringLn (unlines (map showList (pascal 10)));
+main : IO :=
+  printStringLn (unlines (map showList (pascal 10)));

examples/milestone/TicTacToe/CLI/TicTacToe.juvix

@@ -10,37 +10,34 @@ import Stdlib.Prelude open;
 import Logic.Game open;
 
 --- A ;String; that prompts the user for their input
-prompt : GameState → String;
-prompt x :=
-  "\n"
-    ++str showGameState x
-    ++str "\nPlayer "
-    ++str showSymbol (player x)
-    ++str ": ";
+prompt : GameState → String
+  | x :=
+    "\n"
+      ++str showGameState x
+      ++str "\nPlayer "
+      ++str showSymbol (player x)
+      ++str ": ";
 
-nextMove : GameState → String → GameState;
-nextMove s := flip playMove s ∘ validMove ∘ stringToNat;
+nextMove : GameState → String → GameState
+  | s := flip playMove s ∘ validMove ∘ stringToNat;
 
 --- Main loop
 terminating
-run : GameState → IO;
-run (state b p (terminate msg)) :=
-  printStringLn
-    ("\n"
-      ++str showGameState (state b p noError)
-      ++str "\n"
-      ++str msg);
-run (state b p (continue msg)) :=
-  printString (msg ++str prompt (state b p noError))
-    >> readLn (run ∘ nextMove (state b p noError));
-run x :=
-  printString (prompt x) >> readLn (run ∘ nextMove x);
+run : GameState → IO
+  | (state b p (terminate msg)) :=
+    printStringLn
+      ("\n"
+        ++str showGameState (state b p noError)
+        ++str "\n"
+        ++str msg)
+  | (state b p (continue msg)) :=
+    printString (msg ++str prompt (state b p noError))
+      >> readLn (run ∘ nextMove (state b p noError))
+  | x := printString (prompt x) >> readLn (run ∘ nextMove x);
 
 --- The welcome message
-welcome : String;
-welcome :=
+welcome : String :=
   "MiniTicTacToe\n-------------\n\nType a number then ENTER to make a move";
 
 --- The entry point of the program
-main : IO;
-main := printStringLn welcome >> run beginState;
+main : IO := printStringLn welcome >> run beginState;

examples/milestone/TicTacToe/Logic/Board.juvix

@@ -11,34 +11,33 @@ type Board :=
   | board : List (List Square) → Board;
 
 --- Returns the list of numbers corresponding to the empty ;Square;s
-possibleMoves : List Square → List Nat;
-possibleMoves nil := nil;
-possibleMoves (empty n :: xs) := n :: possibleMoves xs;
-possibleMoves (_ :: xs) := possibleMoves xs;
+possibleMoves : List Square → List Nat
+  | nil := nil
+  | (empty n :: xs) := n :: possibleMoves xs
+  | (_ :: xs) := possibleMoves xs;
 
 --- ;true; if all the ;Square;s in the list are equal
-full : List Square → Bool;
-full (a :: b :: c :: nil) := ==Square a b && ==Square b c;
-full _ := fail "full";
+full : List Square → Bool
+  | (a :: b :: c :: nil) := ==Square a b && ==Square b c
+  | _ := fail "full";
 
-diagonals : List (List Square) → List (List Square);
-diagonals ((a1 :: _ :: b1 :: nil)
+diagonals : List (List Square) → List (List Square)
+  | ((a1 :: _ :: b1 :: nil)
     :: (_ :: c :: _ :: nil)
     :: (b2 :: _ :: a2 :: nil)
     :: nil) :=
-  (a1 :: c :: a2 :: nil) :: (b1 :: c :: b2 :: nil) :: nil;
-diagonals _ := fail "diagonals";
+    (a1 :: c :: a2 :: nil) :: (b1 :: c :: b2 :: nil) :: nil
+  | _ := fail "diagonals";
 
-columns : List (List Square) → List (List Square);
-columns := transpose;
+columns : List (List Square) → List (List Square) :=
+  transpose;
 
-rows : List (List Square) → List (List Square);
-rows := id;
+rows : List (List Square) → List (List Square) := id;
 
 --- Textual representation of a ;List Square;
-showRow : List Square → String;
-showRow xs := concat (surround "|" (map showSquare xs));
+showRow : List Square → String
+  | xs := concat (surround "|" (map showSquare xs));
 
-showBoard : Board → String;
-showBoard (board squares) :=
-  unlines (surround "+---+---+---+" (map showRow squares));
+showBoard : Board → String
+  | (board squares) :=
+    unlines (surround "+---+---+---+" (map showRow squares));

examples/milestone/TicTacToe/Logic/Extra.juvix

@@ -8,13 +8,12 @@ import Stdlib.Prelude open;
 --- ;concat (("a" :: nil) :: "b" :: nil); evaluates to ;"a"
   :: "b"
   :: nil;
-concat : List String → String;
-concat := foldl (++str) "";
+concat : List String → String := foldl (++str) "";
 
 --- It inserts the first ;String; at the beginning, in between, and at the end of the second list
-surround : String → List String → List String;
-surround x xs := (x :: intersperse x xs) ++ x :: nil;
+surround : String → List String → List String
+  | x xs := (x :: intersperse x xs) ++ x :: nil;
 
 --- It inserts the first ;String; in between the ;String;s in the second list and concatenates the result
-intercalate : String → List String → String;
-intercalate sep xs := concat (intersperse sep xs);
+intercalate : String → List String → String
+  | sep xs := concat (intersperse sep xs);

examples/milestone/TicTacToe/Logic/Game.juvix

@@ -11,37 +11,37 @@ import Logic.Board open public;
 import Logic.GameState open public;
 
 --- Checks if we reached the end of the game.
-checkState : GameState → GameState;
-checkState (state b p e) :=
-  if
-    (won (state b p e))
-    (state
-      b
-      p
-      (terminate
-        ("Player " ++str showSymbol (switch p) ++str " wins!")))
-    (if
-      (draw (state b p e))
-      (state b p (terminate "It's a draw!"))
-      (state b p e));
+checkState : GameState → GameState
+  | (state b p e) :=
+    if
+      (won (state b p e))
+      (state
+        b
+        p
+        (terminate
+          ("Player " ++str showSymbol (switch p) ++str " wins!")))
+      (if
+        (draw (state b p e))
+        (state b p (terminate "It's a draw!"))
+        (state b p e));
 
 --- Given a player attempted move, updates the state accordingly.
-playMove : Maybe Nat → GameState → GameState;
-playMove nothing (state b p _) :=
-  state b p (continue "\nInvalid number, try again\n");
-playMove (just k) (state (board s) player e) :=
-  if
-    (not (elem (==) k (possibleMoves (flatten s))))
-    (state
-      (board s)
-      player
-      (continue "\nThe square is already occupied, try again\n"))
-    (checkState
+playMove : Maybe Nat → GameState → GameState
+  | nothing (state b p _) :=
+    state b p (continue "\nInvalid number, try again\n")
+  | (just k) (state (board s) player e) :=
+    if
+      (not (elem (==) k (possibleMoves (flatten s))))
       (state
-        (board (map (map (replace player k)) s))
-        (switch player)
-        noError));
+        (board s)
+        player
+        (continue "\nThe square is already occupied, try again\n"))
+      (checkState
+        (state
+          (board (map (map (replace player k)) s))
+          (switch player)
+          noError));
 
 --- Returns ;just; if the given ;Nat; is in range of 1..9
-validMove : Nat → Maybe Nat;
-validMove n := if (n <= 9 && n >= 1) (just n) nothing;
+validMove : Nat → Maybe Nat
+  | n := if (n <= 9 && n >= 1) (just n) nothing;

examples/milestone/TicTacToe/Logic/GameState.juvix

@@ -16,16 +16,15 @@ type GameState :=
   | state : Board → Symbol → Error → GameState;
 
 --- Textual representation of a ;GameState;
-showGameState : GameState → String;
-showGameState (state b _ _) := showBoard b;
+showGameState : GameState → String
+  | (state b _ _) := showBoard b;
 
 --- Projects the player
-player : GameState → Symbol;
-player (state _ p _) := p;
+player : GameState → Symbol
+  | (state _ p _) := p;
 
 --- initial ;GameState;
-beginState : GameState;
-beginState :=
+beginState : GameState :=
   state
     (board
       (map
@@ -38,13 +37,13 @@ beginState :=
     noError;
 
 --- ;true; if some player has won the game
-won : GameState → Bool;
-won (state (board squares) _ _) :=
-  any
-    full
-    (diagonals squares ++ rows squares ++ columns squares);
+won : GameState → Bool
+  | (state (board squares) _ _) :=
+    any
+      full
+      (diagonals squares ++ rows squares ++ columns squares);
 
 --- ;true; if there is a draw
-draw : GameState → Bool;
-draw (state (board squares) _ _) :=
-  null (possibleMoves (flatten squares));
+draw : GameState → Bool
+  | (state (board squares) _ _) :=
+    null (possibleMoves (flatten squares));

examples/milestone/TicTacToe/Logic/Square.juvix

@@ -13,20 +13,20 @@ type Square :=
     occupied : Symbol → Square;
 
 --- Equality for ;Square;s
-==Square : Square → Square → Bool;
-==Square (empty m) (empty n) := m == n;
-==Square (occupied s) (occupied t) := ==Symbol s t;
-==Square _ _ := false;
+==Square : Square → Square → Bool
+  | (empty m) (empty n) := m == n
+  | (occupied s) (occupied t) := ==Symbol s t
+  | _ _ := false;
 
 --- Textual representation of a ;Square;
-showSquare : Square → String;
-showSquare (empty n) := " " ++str natToString n ++str " ";
-showSquare (occupied s) := " " ++str showSymbol s ++str " ";
+showSquare : Square → String
+  | (empty n) := " " ++str natToString n ++str " "
+  | (occupied s) := " " ++str showSymbol s ++str " ";
 
-replace : Symbol → Nat → Square → Square;
-replace player k (empty n) :=
-  if
-    (n Stdlib.Data.Nat.Ord.== k)
-    (occupied player)
-    (empty n);
-replace _ _ s := s;
+replace : Symbol → Nat → Square → Square
+  | player k (empty n) :=
+    if
+      (n Stdlib.Data.Nat.Ord.== k)
+      (occupied player)
+      (empty n)
+  | _ _ s := s;

examples/milestone/TicTacToe/Logic/Symbol.juvix

@@ -11,17 +11,17 @@ type Symbol :=
     X : Symbol;
 
 --- Equality for ;Symbol;s
-==Symbol : Symbol → Symbol → Bool;
-==Symbol O O := true;
-==Symbol X X := true;
-==Symbol _ _ := false;
+==Symbol : Symbol → Symbol → Bool
+  | O O := true
+  | X X := true
+  | _ _ := false;
 
 --- Turns ;O; into ;X; and ;X; into ;O;
-switch : Symbol → Symbol;
-switch O := X;
-switch X := O;
+switch : Symbol → Symbol
+  | O := X
+  | X := O;
 
 --- Textual representation of a ;Symbol;
-showSymbol : Symbol → String;
-showSymbol O := "O";
-showSymbol X := "X";
+showSymbol : Symbol → String
+  | O := "O"
+  | X := "X";

examples/milestone/Tutorial/Tutorial.juvix

@@ -8,5 +8,4 @@ import Stdlib.Prelude open;
 -- bring comparison operators on Nat into scope
 import Stdlib.Data.Nat.Ord open;
 
-main : IO;
-main := printStringLn "Hello world!";
+main : IO := printStringLn "Hello world!";

tests/negative/230/Foo/Data/Bool.juvix

@@ -6,20 +6,22 @@ type Bool :=
   | true : Bool
   | false : Bool;
 
-not : Bool → Bool;
-not true := false;
-not false := true;
+not : Bool → Bool
+  | true := false
+  | false := true;
 
 syntax infixr 2 ||;
-|| : Bool → Bool → Bool;
-|| false a := a;
-|| true _ := true;
+
+|| : Bool → Bool → Bool
+  | false a := a
+  | true _ := true;
 
 syntax infixr 2 &&;
-&& : Bool → Bool → Bool;
-&& false _ := false;
-&& true a := a;
 
-if : {A : Type} → Bool → A → A → A;
-if true a _ := a;
-if false _ b := b;
+&& : Bool → Bool → Bool
+  | false _ := false
+  | true a := a;
+
+if : {A : Type} → Bool → A → A → A
+  | true a _ := a
+  | false _ b := b;

tests/negative/258/M.juvix

@@ -4,6 +4,6 @@ type Nat :=
   | O : Nat
   | S : Nat -> Nat;
 
-fun : Nat -> Nat;
-fun (S {S {x}}) := x;
+fun : Nat -> Nat
+  | (S {S {x}}) := x;
 

tests/negative/265/M.juvix

@@ -7,7 +7,7 @@ type Bool :=
 type Pair (A : Type) (B : Type) :=
   | mkPair : A → B → Pair A B;
 
-f : _ → _;
-f (mkPair false true) := true;
-f true := false;
+f : _ → _
+  | (mkPair false true) := true
+  | true := false;
 

tests/negative/AppLeftImplicit.juvix

@@ -1,5 +1,4 @@
 module AppLeftImplicit;
 
-x : Type;
-x := {x};
+x : Type := {x};
 

tests/negative/ConstructorExpectedLeftApplication.juvix

@@ -1,5 +1,5 @@
 module ConstructorExpectedLeftApplication;
 
-f : {A : Type} -> A -> A;
-f (x y) := x;
+f : {A : Type} -> A -> A
+  | (x y) := x;
 

tests/negative/ImplicitPatternLeftApplication.juvix

@@ -1,5 +1,5 @@
 module ImplicitPatternLeftApplication;
 
-f : {A : Type} -> A -> A;
-f ({x} y) := y;
+f : {A : Type} -> A -> A
+  | ({x} y) := y;
 

tests/negative/Internal/ExpectedExplicitArgument.juvix

@@ -3,5 +3,5 @@ module ExpectedExplicitArgument;
 type T (A : Type) :=
   | c : A → T A;
 
-f : {A : Type} → A → T A;
-f {A} a := c {A} {a};
+f : {A : Type} → A → T A
+  | {A} a := c {A} {a};

tests/negative/Internal/ExpectedExplicitPattern.juvix

@@ -3,5 +3,5 @@ module ExpectedExplicitPattern;
 type T (A : Type) :=
   | c : A → T A;
 
-f : {A : Type} → T A → A;
-f {_} {c a} := a;
+f : {A : Type} → T A → A
+  | {_} {c a} := a;

tests/negative/Internal/ExpectedFunctionType.juvix

@@ -6,5 +6,5 @@ type Pair (A : Type) :=
 type B :=
   | b : B;
 
-f : Pair B → Pair B;
-f (mkPair a b) := a b;
+f : Pair B → Pair B
+  | (mkPair a b) := a b;

tests/negative/Internal/FunctionApplied.juvix

@@ -3,5 +3,5 @@ module FunctionApplied;
 type T (A : Type) :=
   | c : A → T A;
 
-f : {A : Type} → A → T A;
-f {A} a := c {(A → A) A} a;
+f : {A : Type} → A → T A
+  | {A} a := c {(A → A) A} a;

tests/negative/Internal/FunctionPattern.juvix

@@ -3,5 +3,5 @@ module FunctionPattern;
 type T :=
   | A : T;
 
-f : (T → T) → T;
-f A := A;
+f : (T → T) → T
+  | A := A;

tests/negative/Internal/IdenFunctionArgsNoExplicit.juvix

@@ -2,9 +2,7 @@ module IdenFunctionArgsNoExplicit;
 
 import Stdlib.Prelude open;
 
-f : {A : Type} → Nat;
-f := zero;
+f : {A : Type} → Nat := zero;
 
-main : Nat;
-main := f;
+main : Nat := f;
 

tests/negative/Internal/LazyBuiltin.juvix

@@ -6,10 +6,10 @@ type Bool :=
   | false : Bool;
 
 builtin bool-if
-if : {A : Type} -> Bool -> A -> A -> A;
-if true x _ := x;
-if false _ x := x;
+if : {A : Type} -> Bool -> A -> A -> A
+  | true x _ := x
+  | false _ x := x;
 
-f : Bool -> Bool;
-f x := if x;
+f : Bool -> Bool
+  | x := if x;
 

tests/negative/Internal/LhsTooManyPatterns.juvix

@@ -3,5 +3,5 @@ module LhsTooManyPatterns;
 type T :=
   | A : T;
 
-f : T → T;
-f A x := A;
+f : T → T
+  | A x := A;

tests/negative/Internal/LiteralInteger.juvix

@@ -2,5 +2,4 @@ module LiteralInteger;
 
 import Stdlib.Prelude open;
 
-h : Nat;
-h := div 1 -2;
+h : Nat := div 1 -2;

tests/negative/Internal/LiteralIntegerString.juvix

@@ -2,8 +2,7 @@ module LiteralIntegerString;
 
 import Stdlib.Prelude open;
 
-f : String -> Nat;
-f _ := 0;
+f : String -> Nat
+  | _ := 0;
 
-g : Nat;
-g := f 2;
+g : Nat := f 2;

tests/negative/Internal/MultiWrongType.juvix

@@ -6,8 +6,6 @@ type A :=
 type B :=
   | b : B;
 
-f : A;
-f := b;
+f : A := b;
 
-g : B;
-g := a;
+g : B := a;

tests/negative/Internal/PatternConstructor.juvix

@@ -6,6 +6,6 @@ type A :=
 type B :=
   | b : B;
 
-f : A → B;
-f b := b;
+f : A → B
+  | b := b;
 

tests/negative/Internal/Positivity/E10.juvix

@@ -3,8 +3,7 @@ module E10;
 type T0 (A : Type) :=
   | t : (A -> T0 A) -> T0 A;
 
-alias : Type -> Type;
-alias := T0;
+alias : Type -> Type := T0;
 
 type T1 :=
   | c : alias T1 -> T1;

tests/negative/Internal/Positivity/E11.juvix

@@ -3,8 +3,8 @@ module E11;
 type T0 (A : Type) :=
   | t : (A -> T0 A) -> T0 _;
 
-alias : Type -> Type -> Type;
-alias A B := A -> B;
+alias : Type -> Type -> Type
+  | A B := A -> B;
 
 type T1 :=
   | c : alias T1 T1 -> _;

tests/negative/Internal/TooManyArguments.juvix

@@ -3,5 +3,5 @@ module TooManyArguments;
 type T (A : Type) :=
   | c : A → T A;
 
-f : {A : Type} → A → T A;
-f {A} a := c {A} a a {a};
+f : {A : Type} → A → T A
+  | {A} a := c {A} a a {a};

tests/negative/Internal/UnsolvedMeta.juvix

@@ -3,6 +3,5 @@ module UnsolvedMeta;
 type Proxy (A : Type) :=
   | x : Proxy A;
 
-t : Proxy _;
-t := x;
+t : Proxy _ := x;
 

tests/negative/Internal/WrongConstructorArity.juvix

@@ -3,5 +3,5 @@ module WrongConstructorArity;
 type T :=
   | A : T → T;
 
-f : T → T;
-f (A i x) := i;
+f : T → T
+  | (A i x) := i;

tests/negative/Internal/WrongType.juvix

@@ -6,5 +6,4 @@ type A :=
 type B :=
   | b : B;
 
-f : A;
-f := b;
+f : A := b;

tests/negative/LetMissingClause.juvix

@@ -1,7 +1,7 @@
 module LetMissingClause;
 
-id : {A : Type} → A → A;
-id {A} :=
-  let
-    id' : A → A;
-  in id';
+id : {A : Type} → A → A
+  | {A} :=
+    let
+      id' : A → A;
+    in id';

tests/negative/Termination/Data/Bool.juvix

@@ -5,19 +5,21 @@ type Bool :=
   | false : Bool;
 
 syntax infixr 2 ||;
-|| : Bool → Bool → Bool;
-|| false a := a;
-|| true _ := true;
+
+|| : Bool → Bool → Bool
+  | false a := a
+  | true _ := true;
 
 syntax infixr 2 &&;
-&& : Bool → Bool → Bool;
-&& false _ := false;
-&& true a := a;
 
-ite : (a : Type) → Bool → a → a → a;
-ite _ true a _ := a;
-ite _ false _ b := b;
+&& : Bool → Bool → Bool
+  | false _ := false
+  | true a := a;
 
-not : Bool → Bool;
-not true := false;
-not false := true;
+ite : (a : Type) → Bool → a → a → a
+  | _ true a _ := a
+  | _ false _ b := b;
+
+not : Bool → Bool
+  | true := false
+  | false := true;

tests/negative/Termination/Data/Nat.juvix

@@ -5,24 +5,26 @@ type ℕ :=
   | suc : ℕ → ℕ;
 
 syntax infixl 6 +;
-+ : ℕ → ℕ → ℕ;
-+ zero b := b;
-+ (suc a) b := suc (a + b);
+
++ : ℕ → ℕ → ℕ
+  | zero b := b
+  | (suc a) b := suc (a + b);
 
 syntax infixl 7 *;
-* : ℕ → ℕ → ℕ;
-* zero b := zero;
-* (suc a) b := b + a * b;
+
+* : ℕ → ℕ → ℕ
+  | zero b := zero
+  | (suc a) b := b + a * b;
 
 import Data.Bool;
 open Data.Bool;
 
-even : ℕ → Bool;
+even : ℕ → Bool
+  
+  | zero := true
+  | (suc n) := odd n;
 
-odd : ℕ → Bool;
-
-even zero := true;
-even (suc n) := odd n;
-
-odd zero := false;
-odd (suc n) := even n;
+odd : ℕ → Bool
+  
+  | zero := false
+  | (suc n) := even n;

tests/negative/Termination/Data/QuickSort.juvix

@@ -10,33 +10,33 @@ type List (A : Type) :=
   | nil : List A
   | cons : A → List A → List A;
 
-filter : (A : Type) → (A → Bool) → List A → List A;
-filter A f nil := nil A;
-filter A f (cons h hs) :=
-  ite
-    (List A)
-    (f h)
-    (cons A h (filter A f hs))
-    (filter A f hs);
+filter : (A : Type) → (A → Bool) → List A → List A
+  | A f nil := nil A
+  | A f (cons h hs) :=
+    ite
+      (List A)
+      (f h)
+      (cons A h (filter A f hs))
+      (filter A f hs);
 
-concat : (A : Type) → List A → List A → List A;
-concat A nil ys := ys;
-concat A (cons x xs) ys := cons A x (concat A xs ys);
+concat : (A : Type) → List A → List A → List A
+  | A nil ys := ys
+  | A (cons x xs) ys := cons A x (concat A xs ys);
 
-ltx : (A : Type) → (A → A → Bool) → A → A → Bool;
-ltx A lessThan x y := lessThan y x;
+ltx : (A : Type) → (A → A → Bool) → A → A → Bool
+  | A lessThan x y := lessThan y x;
 
-gex : (A : Type) → (A → A → Bool) → A → A → Bool;
-gex A lessThan x y := not (ltx A lessThan x y);
+gex : (A : Type) → (A → A → Bool) → A → A → Bool
+  | A lessThan x y := not (ltx A lessThan x y);
 
-quicksort : (A : Type) → (A → A → Bool) → List A → List A;
-quicksort A _ nil := nil A;
-quicksort A _ (cons x nil) := cons A x (nil A);
-quicksort A lessThan (cons x ys) :=
-  concat
-    A
-    (quicksort A lessThan (filter A (ltx A lessThan x) ys))
-    (concat
+quicksort : (A : Type) → (A → A → Bool) → List A → List A
+  | A _ nil := nil A
+  | A _ (cons x nil) := cons A x (nil A)
+  | A lessThan (cons x ys) :=
+    concat
       A
-      (cons A x (nil A))
-      (quicksort A lessThan (filter A (gex A lessThan x)) ys));
+      (quicksort A lessThan (filter A (ltx A lessThan x) ys))
+      (concat
+        A
+        (cons A x (nil A))
+        (quicksort A lessThan (filter A (gex A lessThan x)) ys));

tests/negative/Termination/Data/Tree.juvix

@@ -4,11 +4,11 @@ type Tree (A : Type) :=
   | leaf : Tree A
   | branch : Tree A → Tree A → Tree A;
 
-f : (A : Type) → Tree A → Tree A → Tree A;
-f A x leaf := x;
-f A x (branch y z) := f A (f A x y) z;
+f : (A : Type) → Tree A → Tree A → Tree A
+  | A x leaf := x
+  | A x (branch y z) := f A (f A x y) z;
 
-g : (A : Type) → Tree A → Tree A → Tree A;
-g A x leaf := x;
-g A x (branch y z) := g A z (g A x y);
+g : (A : Type) → Tree A → Tree A → Tree A
+  | A x leaf := x
+  | A x (branch y z) := g A z (g A x y);
 

tests/negative/Termination/Mutual.juvix

@@ -2,11 +2,10 @@ module Mutual;
 
 axiom A : Type;
 
-f : A -> A -> A;
+f : A -> A -> A
+  
+  | x y := g x (f x x);
 
-g : A -> A -> A;
-
-g x y := f x x;
-
-f x y := g x (f x x);
+g : A -> A -> A
+  | x y := f x x;
 

tests/negative/Termination/Ord.juvix

@@ -8,13 +8,13 @@ type Ord :=
   | SOrd : Ord -> Ord
   | Lim : (ℕ -> Ord) -> Ord;
 
-addord : Ord -> Ord -> Ord;
+addord : Ord -> Ord -> Ord
+  
+  | Zord y := y
+  | (SOrd x) y := SOrd (addord x y)
+  | (Lim f) y := Lim (aux-addord f y);
 
-aux-addord : (ℕ -> Ord) -> Ord -> ℕ -> Ord;
-
-addord Zord y := y;
-addord (SOrd x) y := SOrd (addord x y);
-addord (Lim f) y := Lim (aux-addord f y);
-
-aux-addord f y z := addord (f z) y;
+aux-addord : (ℕ -> Ord) -> Ord -> ℕ -> Ord
+  
+  | f y z := addord (f z) y;
 

tests/negative/Termination/TerminatingF.juvix

@@ -3,11 +3,10 @@ module TerminatingF;
 axiom A : Type;
 
 terminating
-f : A -> A -> A;
+f : A -> A -> A
+  
+  | x y := g x (f x x);
 
-g : A -> A -> A;
-
-g x y := f x x;
-
-f x y := g x (f x x);
+g : A -> A -> A
+  | x y := f x x;
 

tests/negative/Termination/TerminatingG.juvix

@@ -2,12 +2,11 @@ module TerminatingG;
 
 axiom A : Type;
 
-f : A -> A -> A;
+f : A -> A -> A
+  
+  | x y := g x (f x x);
 
 terminating
-g : A -> A -> A;
-
-g x y := f x x;
-
-f x y := g x (f x x);
+g : A -> A -> A
+  | x y := f x x;
 

tests/negative/issue1337/Braces.juvix

@@ -4,6 +4,6 @@ type Nat :=
   | O : Nat
   | S : Nat -> Nat;
 
-fun : Nat -> Nat;
-fun (S {S {x}}) := x;
+fun : Nat -> Nat
+  | (S {S {x}}) := x;
 

tests/negative/issue1344/D.juvix

@@ -3,6 +3,5 @@ module D;
 import Other;
 import U;
 
-u : Other.Unit;
-u := U.t;
+u : Other.Unit := U.t;
 

tests/negative/issue1344/M.juvix

@@ -5,6 +5,5 @@ import Other;
 type Unit :=
   | t : Unit;
 
-u : Other.Unit;
-u := t;
+u : Other.Unit := t;
 

tests/negative/issue1700/SelfApplication.juvix

@@ -3,6 +3,5 @@ module SelfApplication;
 
 import Stdlib.Prelude open;
 
-main : IO;
-main := printNatLn (λ {x := x x} id (3 + 4));
+main : IO := printNatLn (λ {x := x x} id (3 + 4));
 

tests/positive/265/M.juvix

@@ -7,6 +7,6 @@ type Bool :=
 type Pair (A : Type) (B : Type) :=
   | mkPair : A → B → Pair A B;
 
-f : _ → _;
-f (mkPair false true) := true;
-f _ := false;
+f : _ → _
+  | (mkPair false true) := true
+  | _ := false;

tests/positive/272/M.juvix

@@ -11,12 +11,12 @@ type Nat :=
   | zero : Nat
   | suc : Nat → Nat;
 
-f : _;
-f false false := true;
-f true _ := false;
+f : _
+  | false false := true
+  | true _ := false;
 
 type Pair (A : Type) (B : Type) :=
   | mkPair : A → B → Pair A B;
 
-g : _;
-g (mkPair (mkPair zero false) true) := mkPair false zero;
+g : _
+  | (mkPair (mkPair zero false) true) := mkPair false zero;

tests/positive/Ape.juvix

@@ -20,14 +20,12 @@ axiom ++ : String → String → String;
 
 axiom f : String → String;
 
-x : String;
-x := "" + ("" ++ "");
+x : String := "" + ("" ++ "");
 
 axiom wwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwww : String
   → String;
 
-nesting : String;
-nesting :=
+nesting : String :=
   wwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwww
     (wwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwww
       (wwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwww
@@ -50,8 +48,7 @@ nesting :=
                                         (wwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwww
                                           ("" + "" + "" + "" + ""))))))))))))))))))));
 
-t : String;
-t :=
+t : String :=
   "Hellooooooooo"
     >> "Hellooooooooo"
     >> "Hellooooooooo"

tests/positive/Builtins.juvix

@@ -2,12 +2,11 @@ module Builtins;
 
 import Stdlib.Prelude open;
 
-f : String -> IO;
-f s :=
-  printStringLn
-    (natToString (stringToNat "290" + 3)
-      ++str natToString 7
-      ++str s);
+f : String -> IO
+  | s :=
+    printStringLn
+      (natToString (stringToNat "290" + 3)
+        ++str natToString 7
+        ++str s);
 
-main : IO;
-main := readLn f;
+main : IO := readLn f;

tests/positive/BuiltinsBool.juvix

@@ -6,6 +6,6 @@ type Bool :=
   | false : Bool;
 
 builtin bool-if
-if : {A : Type} → Bool → A → A → A;
-if true t _ := t;
-if false _ e := e;
+if : {A : Type} → Bool → A → A → A
+  | true t _ := t
+  | false _ e := e;

tests/positive/Format.juvix

@@ -17,12 +17,12 @@ import Stdlib.Data.Nat.Ord open;
 -- Lorem ipsum dolor sit amet, consectetur adipiscing elit
 terminating
 -- Comment between terminating and type sig
-go : Nat → Nat → Nat;
-go n s :=
-  if
-    (s < n)
-    (go (sub n 1) s)
-    (go n (sub s n) + go (sub n 1) s);
+go : Nat → Nat → Nat
+  | n s :=
+    if
+      (s < n)
+      (go (sub n 1) s)
+      (go n (sub s n) + go (sub n 1) s);
 
 module {- local module -}
 M;
@@ -32,22 +32,18 @@ M;
 end;
 
 -- qualified commas
-t4 : String;
-t4 := "a" M., "b" M., "c" M., "d";
+t4 : String := "a" M., "b" M., "c" M., "d";
 
 open M;
 
 -- mix qualified and unqualified commas
-t5 : String;
-t5 := "a" M., "b" M., "c", "d";
+t5 : String := "a" M., "b" M., "c", "d";
 
 -- comma chain fits in a line
-t2 : String;
-t2 := "a", "b", "c", "d";
+t2 : String := "a", "b", "c", "d";
 
 -- comma chain does not fit in a line
-t3 : String;
-t3 :=
+t3 : String :=
   "a"
     , "b"
     , "c"
@@ -62,8 +58,7 @@ t3 :=
     , "1234";
 
 -- escaping in String literals
-e1 : String;
-e1 := "\"\n";
+e1 : String := "\"\n";
 
 syntax infixl 7 +l7;
 axiom +l7 : String → String → String;
@@ -81,8 +76,7 @@ syntax infixr 6 +r6;
 axiom +r6 : String → String → String;
 
 -- nesting of chains
-t : String;
-t :=
+t : String :=
   "Hellooooooooo"
     +l1 "Hellooooooooo"
     +l1 "Hellooooooooo"
@@ -99,12 +93,12 @@ t :=
       , "hi";
 
 -- function with single wildcard parameter
-g : (_ : Type) -> Nat;
-g _ := 1;
+g : (_ : Type) -> Nat
+  | _ := 1;
 
 -- grouping of type arguments
-exampleFunction1 :
-  {A : Type}
+exampleFunction1
+  : {A : Type}
     -> List A
     -> List A
     -> List A
@@ -112,8 +106,8 @@ exampleFunction1 :
     -> List A
     -> List A
     -> List A
-    -> Nat;
-exampleFunction1 _ _ _ _ _ _ _ := 1;
+    -> Nat
+  | _ _ _ _ _ _ _ := 1;
 
 axiom undefined : {A : Type} -> A;
 
@@ -149,12 +143,10 @@ type T0 (A : Type) :=
   | c0 : (A -> T0 A) -> T0 A;
 
 -- Single Lambda clause
-idLambda : {A : Type} -> A -> A;
-idLambda := λ {x := x};
+idLambda : {A : Type} -> A -> A := λ {x := x};
 
 -- Lambda clauses
-f : Nat -> Nat;
-f :=
+f : Nat -> Nat :=
   \ {
     -- comment before lambda pipe
     | zero :=
@@ -171,15 +163,14 @@ module Patterns;
   type × (A : Type) (B : Type) :=
     | , : A → B → A × B;
 
-  f : Nat × Nat × Nat × Nat -> Nat;
-  f (a, b, c, d) := a;
+  f : Nat × Nat × Nat × Nat -> Nat
+    | (a, b, c, d) := a;
 end;
 
 import Stdlib.Prelude open using {Nat as Natural};
 
 module UnicodeStrings;
-  a : String;
-  a := "λ";
+  a : String := "λ";
 end;
 
 module Comments;
@@ -194,12 +185,11 @@ module Comments;
   axiom a3 -- comment before axiom :
   : Type;
 
-  num -- comment before type sig :
-  :
-    -- comment after type sig :
-    Nat;
-  num -- comment before clause :=
-  :=
+  num
+    -- comment before type sig :
+    : -- comment after type sig :
+    Nat :=
+    -- comment before clause :=
     -- comment after clause :=
     123;
 
@@ -214,16 +204,16 @@ module Comments;
     : Type}
     -> Type;
 
-  id2 : {A : Type} -> A -> Nat -> A;
-  id2 -- before patternarg braces
+  id2 : {A : Type} -> A -> Nat -> A
+    | -- before patternarg braces
     {A} a -- before open patternarg parens
     (suc b) :=
-    idLambda
-      -- before implicit app
-      {-- inside implicit arg
-      A}
-      -- before closing implicit arg
-      a;
+      idLambda
+        -- before implicit app
+        {-- inside implicit arg
+        A}
+        -- before closing implicit arg
+        a;
 
   type color : Type :=
     -- comment before pipe

tests/positive/IdInType.juvix

@@ -3,8 +3,8 @@ module IdInType;
 type Unit :=
   | unit : Unit;
 
-id : {a : Type} -> a -> a;
-id a := a;
+id : {a : Type} -> a -> a
+  | a := a;
 
-f : id Unit -> Unit;
-f _ := unit;
+f : id Unit -> Unit
+  | _ := unit;

tests/positive/ImportAsOpen/Main.juvix

@@ -2,8 +2,6 @@ module Main;
 
 import Other as O open;
 
-B : Type;
-B := A;
+B : Type := A;
 
-B' : Type;
-B' := O.A;
+B' : Type := O.A;

tests/positive/ImportShadow/Main.juvix

@@ -5,17 +5,15 @@ import Nat open;
 type Unit :=
   | unit : Unit;
 
-f : Nat;
-f :=
+f : Nat :=
   case unit
     | is-zero := zero;
 
-f2 : Nat;
-f2 :=
+f2 : Nat :=
   case suc zero
     | suc is-zero := zero
     | _ := zero;
 
-f3 : Nat → Nat;
-f3 (suc is-zero) := is-zero;
-f3 zero := zero;
+f3 : Nat → Nat
+  | (suc is-zero) := is-zero
+  | zero := zero;

tests/positive/ImportShadow/Nat.juvix

@@ -8,8 +8,8 @@ type Nat :=
   | zero : Nat
   | suc : Nat → Nat;
 
-is-zero : Nat → Bool;
-is-zero n :=
-  case n
-    | zero := true
-    | suc _ := false;
+is-zero : Nat → Bool
+  | n :=
+    case n
+      | zero := true
+      | suc _ := false;

tests/positive/Imports/A.juvix

@@ -13,5 +13,5 @@ end;
 
 import M;
 
-f : M.N.T;
-f (_ M.N.t _) := Type M.+ Type M.+ M.MType;
+f : M.N.T
+  | (_ M.N.t _) := Type M.+ Type M.+ M.MType;

tests/positive/Internal/AsPattern.juvix

@@ -1,15 +1,16 @@
 module AsPattern;
 
 syntax infixr 9 ∘;
-∘ :
-  {A : Type}
+
+∘
+  : {A : Type}
     → {B : Type}
     → {C : Type}
     → (B → C)
     → (A → B)
     → A
-    → C;
-∘ {_} {B} {_} f g x := f (g x);
+    → C
+  | {_} {B} {_} f g x := f (g x);
 
 builtin nat
 type Nat :=
@@ -17,27 +18,28 @@ type Nat :=
   | suc : Nat → Nat;
 
 syntax infixl 6 +;
+
 builtin nat-plus
-+ : Nat → Nat → Nat;
-+ zero b := b;
-+ (suc a) b := suc (a + b);
++ : Nat → Nat → Nat
+  | zero b := b
+  | (suc a) b := suc (a + b);
 
 syntax infixr 2 ×;
 syntax infixr 4 ,;
 type × (A : Type) (B : Type) :=
   | , : A → B → A × B;
 
-fst : {A : Type} → {B : Type} → A × B → A;
-fst p@(a, _) := a;
+fst : {A : Type} → {B : Type} → A × B → A
+  | p@(a, _) := a;
 
-snd : {A : Type} → {B : Type} → A × B → B;
-snd p@(_, b) := b;
+snd : {A : Type} → {B : Type} → A × B → B
+  | p@(_, b) := b;
 
-lambda : Nat → Nat → Nat;
-lambda x := λ {a@(suc _) := a + x + zero};
+lambda : Nat → Nat → Nat
+  | x := λ {a@(suc _) := a + x + zero};
 
-a : {A : Type} → A × Nat → Nat;
-a p@(x, s@zero) := snd p + 1;
+a : {A : Type} → A × Nat → Nat
+  | p@(x, s@zero) := snd p + 1;
 
-b : {A : Type} → A × Nat → ({B : Type} → B → B) → A;
-b p@(_, zero) f := (f ∘ fst) p;
+b : {A : Type} → A × Nat → ({B : Type} → B → B) → A
+  | p@(_, zero) f := (f ∘ fst) p;

tests/positive/Internal/Box.juvix

@@ -6,11 +6,9 @@ type Box (A : Type) :=
 type T :=
   | t : T;
 
-b : Box _;
-b := box t;
+b : Box _ := box t;
 
-id : {A : Type} → A → A;
-id x := x;
+id : {A : Type} → A → A
+  | x := x;
 
-tt : _;
-tt := id t;
+tt : _ := id t;

tests/positive/Internal/Case.juvix

@@ -2,41 +2,41 @@ module Case;
 
 import Stdlib.Prelude open;
 
-isZero : Nat → Bool;
-isZero n :=
-  case n
-    | zero := true
-    | k@(suc _) := false;
+isZero : Nat → Bool
+  | n :=
+    case n
+      | zero := true
+      | k@(suc _) := false;
 
-id' : Bool → {A : Type} → A → A;
-id' b :=
-  case b
-    | true := id
-    | false := id;
+id' : Bool → {A : Type} → A → A
+  | b :=
+    case b
+      | true := id
+      | false := id;
 
-pred : Nat → Nat;
-pred n :=
-  case n
-    | zero := zero
-    | suc n := n;
+pred : Nat → Nat
+  | n :=
+    case n
+      | zero := zero
+      | suc n := n;
 
-appIf : {A : Type} → Bool → (A → A) → A → A;
-appIf b f :=
-  case b
-    | true := f
-    | false := id;
-
-appIf2 : {A : Type} → Bool → (A → A) → A → A;
-appIf2 b f a :=
-  (case b
+appIf : {A : Type} → Bool → (A → A) → A → A
+  | b f :=
+    case b
       | true := f
-      | false := id)
-    a;
+      | false := id;
 
-nestedCase1 : {A : Type} → Bool → (A → A) → A → A;
-nestedCase1 b f :=
-  case b
-    | true :=
-      (case b
-        | _ := id)
-    | false := id;
+appIf2 : {A : Type} → Bool → (A → A) → A → A
+  | b f a :=
+    (case b
+        | true := f
+        | false := id)
+      a;
+
+nestedCase1 : {A : Type} → Bool → (A → A) → A → A
+  | b f :=
+    case b
+      | true :=
+        (case b
+          | _ := id)
+      | false := id;

tests/positive/Internal/HoleInSignature.juvix

@@ -7,8 +7,7 @@ type Bool :=
   | true : Bool
   | false : Bool;
 
-p : Pair _ _;
-p := mkPair true false;
+p : Pair _ _ := mkPair true false;
 
-p2 : (A : Type) → (B : Type) → _ → B → Pair A _;
-p2 _ _ a b := mkPair a b;
+p2 : (A : Type) → (B : Type) → _ → B → Pair A _
+  | _ _ a b := mkPair a b;

tests/positive/Internal/Implicit.juvix

@@ -1,15 +1,16 @@
 module Implicit;
 
 syntax infixr 9 ∘;
-∘ :
-  {A : Type}
+
+∘
+  : {A : Type}
     → {B : Type}
     → {C : Type}
     → (B → C)
     → (A → B)
     → A
-    → C;
-∘ f g x := f (g x);
+    → C
+  | f g x := f (g x);
 
 type Nat :=
   | zero : Nat
@@ -20,126 +21,119 @@ syntax infixr 4 ,;
 type × (A : Type) (B : Type) :=
   | , : A → B → A × B;
 
-uncurry :
-  {A : Type}
+uncurry
+  : {A : Type}
     → {B : Type}
     → {C : Type}
     → (A → B → C)
     → A × B
-    → C;
-uncurry f (a, b) := f a b;
+    → C
+  | f (a, b) := f a b;
 
-fst : {A : Type} → {B : Type} → A × B → A;
-fst (a, _) := a;
+fst : {A : Type} → {B : Type} → A × B → A
+  | (a, _) := a;
 
-snd : {A : Type} → {B : Type} → A × B → B;
-snd (_, b) := b;
+snd : {A : Type} → {B : Type} → A × B → B
+  | (_, b) := b;
 
-swap : {A : Type} → {B : Type} → A × B → B × A;
-swap (a, b) := b, a;
+swap : {A : Type} → {B : Type} → A × B → B × A
+  | (a, b) := b, a;
 
-first :
-  {A : Type}
+first
+  : {A : Type}
     → {B : Type}
     → {A' : Type}
     → (A → A')
     → A × B
-    → A' × B;
-first f (a, b) := f a, b;
+    → A' × B
+  | f (a, b) := f a, b;
 
-second :
-  {A : Type}
+second
+  : {A : Type}
     → {B : Type}
     → {B' : Type}
     → (B → B')
     → A × B
-    → A × B';
-second f (a, b) := a, f b;
+    → A × B'
+  | f (a, b) := a, f b;
 
-both : {A : Type} → {B : Type} → (A → B) → A × A → B × B;
-both f (a, b) := f a, f b;
+both : {A : Type} → {B : Type} → (A → B) → A × A → B × B
+  | f (a, b) := f a, f b;
 
 type Bool :=
   | true : Bool
   | false : Bool;
 
-if : {A : Type} → Bool → A → A → A;
-if true a _ := a;
-if false _ b := b;
+if : {A : Type} → Bool → A → A → A
+  | true a _ := a
+  | false _ b := b;
 
 syntax infixr 5 ::;
 type List (A : Type) :=
   | nil : List A
   | :: : A → List A → List A;
 
-upToTwo : _;
-upToTwo := zero :: suc zero :: suc (suc zero) :: nil;
+upToTwo : _ := zero :: suc zero :: suc (suc zero) :: nil;
 
-p1 : Nat → Nat → Nat × Nat;
-p1 a b := a, b;
+p1 : Nat → Nat → Nat × Nat
+  | a b := a, b;
 
 type Proxy (A : Type) :=
   | proxy : Proxy A;
 
-t2' : {A : Type} → Proxy A;
-t2' := proxy;
+t2' : {A : Type} → Proxy A := proxy;
 
-t2 : {A : Type} → Proxy A;
-t2 := proxy;
+t2 : {A : Type} → Proxy A := proxy;
 
-t3 :
-  ({A : Type} → Proxy A) → {B : Type} → Proxy B → Proxy B;
-t3 _ _ := proxy;
+t3 : ({A : Type} → Proxy A) → {B : Type} → Proxy B → Proxy B
+  | _ _ := proxy;
 
-t4 : {B : Type} → Proxy B;
-t4 {_} := t3 proxy proxy;
+t4 : {B : Type} → Proxy B
+  | {_} := t3 proxy proxy;
 
-t4' : {B : Type} → Proxy B;
-t4' := t3 proxy proxy;
+t4' : {B : Type} → Proxy B := t3 proxy proxy;
 
-map : {A : Type} → {B : Type} → (A → B) → List A → List B;
-map f nil := nil;
-map f (x :: xs) := f x :: map f xs;
+map : {A : Type} → {B : Type} → (A → B) → List A → List B
+  | f nil := nil
+  | f (x :: xs) := f x :: map f xs;
 
-t : {A : Type} → Proxy A;
-t {_} := proxy;
+t : {A : Type} → Proxy A
+  | {_} := proxy;
 
-t' : {A : Type} → Proxy A;
-t' := proxy;
+t' : {A : Type} → Proxy A := proxy;
 
-t5 : {A : Type} → Proxy A → Proxy A;
-t5 p := p;
+t5 : {A : Type} → Proxy A → Proxy A
+  | p := p;
 
-t5' : {A : Type} → Proxy A → Proxy A;
-t5' proxy := proxy;
+t5' : {A : Type} → Proxy A → Proxy A
+  | proxy := proxy;
 
-f : {A : Type} → {B : Type} → A → B → _;
-f a b := a;
+f : {A : Type} → {B : Type} → A → B → _
+  | a b := a;
 
-pairEval : {A : Type} → {B : Type} → (A → B) × A → B;
-pairEval (f, x) := f x;
+pairEval : {A : Type} → {B : Type} → (A → B) × A → B
+  | (f, x) := f x;
 
-pairEval' :
-  {A : Type} → {B : Type} → ({C : Type} → A → B) × A → B;
-pairEval' (f, x) := f {Nat} x;
+pairEval'
+  : {A : Type} → {B : Type} → ({C : Type} → A → B) × A → B
+  | (f, x) := f {Nat} x;
 
-foldr :
-  {A : Type} → {B : Type} → (A → B → B) → B → List A → B;
-foldr _ z nil := z;
-foldr f z (h :: hs) := f h (foldr f z hs);
+foldr
+  : {A : Type} → {B : Type} → (A → B → B) → B → List A → B
+  | _ z nil := z
+  | f z (h :: hs) := f h (foldr f z hs);
 
-foldl :
-  {A : Type} → {B : Type} → (B → A → B) → B → List A → B;
-foldl f z nil := z;
-foldl f z (h :: hs) := foldl f (f z h) hs;
+foldl
+  : {A : Type} → {B : Type} → (B → A → B) → B → List A → B
+  | f z nil := z
+  | f z (h :: hs) := foldl f (f z h) hs;
 
-filter : {A : Type} → (A → Bool) → List A → List A;
-filter _ nil := nil;
-filter f (h :: hs) :=
-  if (f h) (h :: filter f hs) (filter f hs);
+filter : {A : Type} → (A → Bool) → List A → List A
+  | _ nil := nil
+  | f (h :: hs) := if (f h) (h :: filter f hs) (filter f hs);
 
-partition :
-  {A : Type} → (A → Bool) → List A → List A × List A;
-partition _ nil := nil, nil;
-partition f (x :: xs) :=
-  if (f x) first second ((::) x) (partition f xs);
+partition
+  : {A : Type} → (A → Bool) → List A → List A × List A
+  | _ nil := nil, nil
+  | f (x :: xs) :=
+    if (f x) first second ((::) x) (partition f xs);

tests/positive/Internal/Lambda.juvix

@@ -10,103 +10,104 @@ type × (A : Type) (B : Type) :=
   | , : A → B → A × B;
 
 syntax infixr 9 ∘;
-∘ :
-  {A : Type}
+
+∘
+  : {A : Type}
     → {B : Type}
     → {C : Type}
     → (B → C)
     → (A → B)
     → A
-    → C;
-∘ {_} {B} {_} := λ {f g x := f (g x)};
+    → C
+  | {_} {B} {_} := λ {f g x := f (g x)};
 
-id : {A : Type} → A → A;
-id := λ {a := a};
+id : {A : Type} → A → A := λ {a := a};
 
-id2 : {A : Type} → {B : Type} → A → A;
-id2 := λ {a := a};
+id2 : {A : Type} → {B : Type} → A → A := λ {a := a};
 
-id' : (A : Type) → A → A;
-id' := λ {A a := a};
+id' : (A : Type) → A → A := λ {A a := a};
 
-id'' : (A : Type) → A → A;
-id'' := λ {A := λ {a := a}};
+id'' : (A : Type) → A → A := λ {A := λ {a := a}};
 
-uncurry :
-  {A : Type}
+uncurry
+  : {A : Type}
     → {B : Type}
     → {C : Type}
     → (A → B → C)
     → A × B
-    → C;
-uncurry := λ {f (a, b) := f a b};
+    → C := λ {f (a, b) := f a b};
 
-idB : {A : Type} → A → A;
-idB a := λ {a := a} a;
+idB : {A : Type} → A → A
+  | a := λ {a := a} a;
 
-mapB : {A : Type} → (A → A) → A → A;
-mapB := λ {f a := f a};
+mapB : {A : Type} → (A → A) → A → A := λ {f a := f a};
 
-add : Nat → Nat → Nat;
-add :=
+add : Nat → Nat → Nat :=
   λ {
     | zero n := n
     | (suc n) := λ {m := suc (add n m)}
   };
 
-fst : {A : Type} → {B : Type} → A × B → A;
-fst {_} := λ {(a, _) := a};
+fst : {A : Type} → {B : Type} → A × B → A
+  | {_} := λ {(a, _) := a};
 
-swap : {A : Type} → {B : Type} → A × B → B × A;
-swap {_} {_} := λ {(a, b) := b, a};
+swap : {A : Type} → {B : Type} → A × B → B × A
+  | {_} {_} := λ {(a, b) := b, a};
 
-first :
-  {A : Type}
+first
+  : {A : Type}
     → {B : Type}
     → {A' : Type}
     → (A → A')
     → A × B
-    → A' × B;
-first := λ {f (a, b) := f a, b};
+    → A' × B := λ {f (a, b) := f a, b};
 
-second :
-  {A : Type}
+second
+  : {A : Type}
     → {B : Type}
     → {B' : Type}
     → (B → B')
     → A × B
-    → A × B';
-second f (a, b) := a, f b;
+    → A × B'
+  | f (a, b) := a, f b;
 
-both : {A : Type} → {B : Type} → (A → B) → A × A → B × B;
-both {_} {B} := λ {f (a, b) := f a, f b};
+both : {A : Type} → {B : Type} → (A → B) → A × A → B × B
+  | {_} {B} := λ {f (a, b) := f a, f b};
 
 syntax infixr 5 ::;
 type List (a : Type) :=
   | nil : List a
   | :: : a → List a → List a;
 
-map : {A : Type} → {B : Type} → (A → B) → List A → List B;
-map {_} :=
-  λ {
-    | f nil := nil
-    | f (x :: xs) := f x :: map f xs
-  };
+map : {A : Type} → {B : Type} → (A → B) → List A → List B
+  | {_} :=
+    λ {
+      | f nil := nil
+      | f (x :: xs) := f x :: map f xs
+    };
 
-pairEval : {A : Type} → {B : Type} → (A → B) × A → B;
-pairEval := λ {(f, x) := f x};
+pairEval : {A : Type} → {B : Type} → (A → B) × A → B :=
+  λ {(f, x) := f x};
 
-foldr :
-  {A : Type} → {B : Type} → (A → B → B) → B → List A → B;
-foldr :=
+foldr
+  : {A : Type}
+    → {B : Type}
+    → (A → B → B)
+    → B
+    → List A
+    → B :=
   λ {
     | _ z nil := z
     | f z (h :: hs) := f h (foldr f z hs)
   };
 
-foldl :
-  {A : Type} → {B : Type} → (B → A → B) → B → List A → B;
-foldl :=
+foldl
+  : {A : Type}
+    → {B : Type}
+    → (B → A → B)
+    → B
+    → List A
+    → B :=
   λ {
     | f z nil := z
     | f z (h :: hs) := foldl f (f z h) hs
@@ -116,56 +117,51 @@ type Bool :=
   | true : Bool
   | false : Bool;
 
-if : {A : Type} → Bool → A → A → A;
-if :=
+if : {A : Type} → Bool → A → A → A :=
   λ {
     | true a _ := a
     | false _ b := b
   };
 
-filter : {A : Type} → (A → Bool) → List A → List A;
-filter :=
+filter : {A : Type} → (A → Bool) → List A → List A :=
   λ {
     | _ nil := nil
     | f (h :: hs) := if (f h) (h :: filter f hs) (filter f hs)
   };
 
-partition :
-  {A : Type} → (A → Bool) → List A → List A × List A;
-partition :=
+partition
+  : {A : Type} → (A → Bool) → List A → List A × List A :=
   λ {
     | _ nil := nil, nil
     | f (x :: xs) :=
       if (f x) first second ((::) x) (partition f xs)
   };
 
-zipWith :
-  {A : Type}
+zipWith
+  : {A : Type}
     → {B : Type}
     → {C : Type}
     → (_ → _ → _)
     → List A
     → List B
-    → List C;
-zipWith :=
+    → List C :=
   λ {
     | _ nil _ := nil
     | _ _ nil := nil
     | f (x :: xs) (y :: ys) := f x y :: zipWith f xs ys
   };
 
-t :
-  {A : Type}
+t
+  : {A : Type}
     → {B : Type}
     → ({X : Type} → List X)
-    → List A × List B;
-t := id {({X : Type} → List X) → _} λ {f := f {_}, f {_}};
+    → List A × List B :=
+  id {({X : Type} → List X) → _} λ {f := f {_}, f {_}};
 
 type Box (A : Type) :=
-  | b : A → Box A;
+  | box : A → Box A;
 
-x : Box ((A : Type) → A → A);
-x := b λ {A a := a};
+x : Box ((A : Type) → A → A) := box λ {A a := a};
 
-t1 : {A : Type} → Box ((A : Type) → A → A) → A → A;
-t1 {A} := λ {(b f) := f A};
+t1 : {A : Type} → Box ((A : Type) → A → A) → A → A
+  | {A} := λ {(box f) := f A};

tests/positive/Internal/LiteralInt.juvix

@@ -8,8 +8,6 @@ type A :=
 type B :=
   | b : B;
 
-f : Nat;
-f := 1;
+f : Nat := 1;
 
-main : IO;
-main := printNatLn 2;
+main : IO := printNatLn 2;

tests/positive/Internal/LiteralString.juvix

@@ -9,5 +9,4 @@ type A :=
 type B :=
   | b : B;
 
-f : String;
-f := "a";
+f : String := "a";

tests/positive/Internal/Mutual.juvix

@@ -8,16 +8,16 @@ type Nat :=
   | zero : Nat
   | suc : Nat → Nat;
 
-not : _;
-not false := true;
-not true := false;
+not : _
+  | false := true
+  | true := false;
 
-odd : _;
+odd : _
+  
+  | zero := false
+  | (suc n) := even n;
 
-even : _;
-
-odd zero := false;
-odd (suc n) := even n;
-
-even zero := true;
-even (suc n) := odd n;
+even : _
+  
+  | zero := true
+  | (suc n) := odd n;

tests/positive/Internal/Norm.juvix

@@ -2,5 +2,4 @@ module Norm;
 
 import Stdlib.Prelude open;
 
-main : Nat;
-main := λ {x := x + 2} 1;
+main : Nat := λ {x := x + 2} 1;

tests/positive/Internal/Simple.juvix

@@ -3,8 +3,7 @@ module Simple;
 type T :=
   | tt : T;
 
-someT : T;
-someT := tt;
+someT : T := tt;
 
 type Bool :=
   | false : Bool
@@ -15,24 +14,25 @@ type Nat :=
   | suc : Nat → Nat;
 
 syntax infix 3 ==;
-== : Nat → Nat → Bool;
-== zero zero := true;
-== (suc a) (suc b) := a == b;
-== _ _ := false;
+
+== : Nat → Nat → Bool
+  | zero zero := true
+  | (suc a) (suc b) := a == b
+  | _ _ := false;
 
 syntax infixl 4 +;
-+ : Nat → Nat → Nat;
-+ zero b := b;
-+ (suc a) b := suc (a + b);
+
++ : Nat → Nat → Nat
+  | zero b := b
+  | (suc a) b := suc (a + b);
 
 syntax infixr 5 ::;
 type List :=
   | nil : List
   | :: : Nat → List → List;
 
-foldr : (Nat → Nat → Nat) → Nat → List → Nat;
-foldr _ v nil := v;
-foldr f v (a :: as) := f a (foldr f v as);
+foldr : (Nat → Nat → Nat) → Nat → List → Nat
+  | _ v nil := v
+  | f v (a :: as) := f a (foldr f v as);
 
-sum : List → Nat;
-sum := foldr (+) zero;
+sum : List → Nat := foldr (+) zero;

tests/positive/Internal/Synonyms.juvix

@@ -2,21 +2,18 @@ module Synonyms;
 
 import Stdlib.Prelude open;
 
-Ty1 : Type;
-Ty1 := Bool → Bool;
+Ty1 : Type := Bool → Bool;
 
-Ty2 : Type;
-Ty2 := Ty1;
+Ty2 : Type := Ty1;
 
-k : Ty2;
-k x := x;
+k : Ty2
+  | x := x;
 
-Num : Type;
-Num := {A : Type} → (A → A) → A → A;
+Num : Type := {A : Type} → (A → A) → A → A;
 
 -- we need the explicit `{_}` since we do not normalize types in the arity checker
-czero : Num;
-czero {_} f x := x;
+czero : Num
+  | {_} f x := x;
 
-csuc : Num → Num;
-csuc n {_} f := f ∘ n {_} f;
+csuc : Num → Num
+  | n {_} f := f ∘ n {_} f;

tests/positive/Iterators.juvix

@@ -1,25 +1,27 @@
 module Iterators;
 
 syntax iterator for {init: 1, range: 1};
-for : {A B : Type} → (A → B → A) → A → B → A;
-for f x y := f x y;
+
+for : {A B : Type} → (A → B → A) → A → B → A
+  | f x y := f x y;
 
 syntax iterator bind {init: 1, range: 0};
-bind : {A B : Type} → (A → B) → A → B;
-bind f x := f x;
+
+bind : {A B : Type} → (A → B) → A → B
+  | f x := f x;
 
 syntax iterator itconst {init: 2, range: 2};
-itconst :
-  {A B C : Type} → (A → A → B → C → A) → A → A → B → C → A;
-itconst f := f;
+
+itconst
+  : {A B C : Type} → (A → A → B → C → A) → A → A → B → C → A
+  | f := f;
 
 builtin bool
 type Bool :=
   | true : Bool
   | false : Bool;
 
-main : Bool;
-main :=
+main : Bool :=
   bind (z := false)
     itconst (a := true; b := false) (c in false; d in false)
       for (x := true) (y in false)

tests/positive/Judoc.juvix

@@ -14,8 +14,8 @@ type T :=
   id; example
 --- hahahah
 --- and another one ;T;
-id : {A : Type} → A → A;
-id a := a;
+id : {A : Type} → A → A
+  | a := a;
 
 --- hellowww
 {-- judoc block --}
@@ -25,9 +25,9 @@ block --}
 {--  --}
 {-- f
 z ;Type; --}
-id2 : {A : Type} → A → A;
-id2 a := a;
-id2 a := a;
+id2 : {A : Type} → A → A
+  | a := a
+  | a := a;
 
 -- }
 --- testing double minus --

tests/positive/LambdaCalculus.juvix

@@ -1,8 +1,8 @@
 module LambdaCalculus;
 
-LambdaTy : Type -> Type;
+LambdaTy : Type -> Type :=  Lambda;
 
-AppTy : Type -> Type;
+AppTy : Type -> Type :=  App;
 
 type Expr (V : Type) :=
   | var : V -> Expr V
@@ -14,7 +14,3 @@ type Lambda (V : Type) :=
 
 type App (V : Type) :=
   | mkApp : Expr V -> Expr V -> App V;
-
-LambdaTy := Lambda;
-
-AppTy := App;

tests/positive/LetShadow.juvix

@@ -7,8 +7,7 @@ type Nat :=
 type Unit :=
   | unit : Unit;
 
-t : Nat;
-t :=
+t : Nat :=
   case unit
     | x :=
       let

tests/positive/Literals.juvix

@@ -6,17 +6,12 @@ axiom String : Type;
 
 axiom + : Int → Int → Int;
 
-a : Int;
-a := 12313;
+a : Int := 12313;
 
-b : Int;
-b := -8;
+b : Int := -8;
 
-- : Int;
-- := 10;
+- : Int := 10;
 
--+-- : Int;
--+-- := - + -+--;
+-+-- : Int := - + -+--;
 
-c : String;
-c := "hellooooo";
+c : String := "hellooooo";

tests/positive/LocalSynonym.juvix

@@ -3,10 +3,8 @@ module LocalSynonym;
 type Unit :=
   | unit : Unit;
 
-myUnit : Type;
-myUnit := Unit;
+myUnit : Type := Unit;
 
 module L;
-  haha : myUnit;
-  haha := unit;
+  haha : myUnit := unit;
 end;

tests/positive/MultiParams.juvix

@@ -3,10 +3,8 @@ module MultiParams;
 type Multi (A B C : Type) :=
   | mult : Multi A B C;
 
-f :
-  {A B : Type} → (C : Type) → {D E F : Type} → Type → Type;
-f C _ := C;
+f : {A B : Type} → (C : Type) → {D E F : Type} → Type → Type
+  | C _ := C;
 
-g :
-  {A B : Type} → (C : Type) → {D _ F : Type} → Type → Type;
-g C _ := C;
+g : {A B : Type} → (C : Type) → {D _ F : Type} → Type → Type
+  | C _ := C;

tests/positive/MutualLet.juvix

@@ -3,8 +3,7 @@ module MutualLet;
 import Stdlib.Data.Nat open;
 import Stdlib.Data.Bool open;
 
-main : _;
-main :=
+main : _ :=
   let
     odd : _;
     even : _;

tests/positive/MutualType.juvix

@@ -8,10 +8,10 @@ type List (a : Type) :=
   | --- An element followed by a list
     :: : a → List a → List a;
 
-Forest : Type -> Type;
+Forest : Type -> Type
+  
+  | A := List (Tree A);
 
 --- N-Ary tree.
 type Tree (A : Type) :=
   | node : A -> Forest A -> Tree A;
-
-Forest A := List (Tree A);

tests/positive/NestedPatterns.juvix

@@ -5,11 +5,11 @@ import Stdlib.Prelude open;
 type MyList (A : Type) :=
   | myList : List A -> MyList A;
 
-toList : {A : Type} -> MyList A -> List A;
-toList (myList xs) := xs;
+toList : {A : Type} -> MyList A -> List A
+  | (myList xs) := xs;
 
-f : MyList Nat -> Nat;
-f xs :=
-  case toList xs
-    | suc n :: nil := n
-    | _ := zero;
+f : MyList Nat -> Nat
+  | xs :=
+    case toList xs
+      | suc n :: nil := n
+      | _ := zero;

tests/positive/Operators.juvix

@@ -3,11 +3,10 @@ module Operators;
 syntax infixl 5 +;
 axiom + : Type → Type → Type;
 
-plus : Type → Type → Type;
-plus := (+);
+plus : Type → Type → Type := (+);
 
-plus2 : Type → Type → Type → Type;
-plus2 a b c := a + b + c;
+plus2 : Type → Type → Type → Type
+  | a b c := a + b + c;
 
-plus3 : Type → Type → Type → Type → Type;
-plus3 a b c d := (+) (a + b) ((+) c d);
+plus3 : Type → Type → Type → Type → Type
+  | a b c d := (+) (a + b) ((+) c d);

tests/positive/Parsing.juvix

@@ -1,7 +1,6 @@
 module Parsing;
 
-let' : Type;
-let' := Type;
+let' : Type := Type;
 
 {- block comment -}
 -- line comment
@@ -23,5 +22,4 @@ block comment 2
 -}
 -}
 
-TypeMine : Type;
-TypeMine := Type;
+TypeMine : Type := Type;

tests/positive/Polymorphism.juvix

@@ -15,105 +15,101 @@ type Bool :=
   | false : Bool
   | true : Bool;
 
-id : (A : Type) → A → A;
-id _ a := a;
+id : (A : Type) → A → A
+  | _ a := a;
 
 terminating
-undefined : (A : Type) → A;
-undefined A := undefined A;
+undefined : (A : Type) → A
+  | A := undefined A;
 
-add : Nat → Nat → Nat;
-add zero b := b;
-add (suc a) b := suc (add a b);
+add : Nat → Nat → Nat
+  | zero b := b
+  | (suc a) b := suc (add a b);
 
-nil' : (E : Type) → List E;
-nil' A := nil;
+nil' : (E : Type) → List E
+  | A := nil;
 
 -- currying
-nil'' : (E : Type) → List E;
-nil'' E := nil;
+nil'' : (E : Type) → List E
+  | E := nil;
 
-fst : (A : Type) → (B : Type) → Pair A B → A;
-fst _ _ (mkPair a b) := a;
+fst : (A : Type) → (B : Type) → Pair A B → A
+  | _ _ (mkPair a b) := a;
 
-p : Pair Bool Bool;
-p := mkPair true false;
+p : Pair Bool Bool := mkPair true false;
 
-swap : (A : Type) → (B : Type) → Pair A B → Pair B A;
-swap A B (mkPair a b) := mkPair b a;
+swap : (A : Type) → (B : Type) → Pair A B → Pair B A
+  | A B (mkPair a b) := mkPair b a;
 
-curry :
-  (A : Type)
+curry
+  : (A : Type)
     → (B : Type)
     → (C : Type)
     → (Pair A B → C)
     → A
     → B
-    → C;
-curry A B C f a b := f (mkPair a b);
+    → C
+  | A B C f a b := f (mkPair a b);
 
-ap : (A : Type) → (B : Type) → (A → B) → A → B;
-ap A B f a := f a;
+ap : (A : Type) → (B : Type) → (A → B) → A → B
+  | A B f a := f a;
 
-ite : (A : Type) → Bool → A → A → A;
-ite _ true tt _ := tt;
-ite _ false _ ff := ff;
+ite : (A : Type) → Bool → A → A → A
+  | _ true tt _ := tt
+  | _ false _ ff := ff;
 
-headDef : (A : Type) → A → List A → A;
-headDef _ d nil := d;
-headDef A _ (cons h _) := h;
+headDef : (A : Type) → A → List A → A
+  | _ d nil := d
+  | A _ (cons h _) := h;
 
-filter : (A : Type) → (A → Bool) → List A → List A;
-filter A f nil := nil;
-filter A f (cons x xs) :=
-  ite
-    (List A)
-    (f x)
-    (cons x (filter A f xs))
-    (filter A f xs);
+filter : (A : Type) → (A → Bool) → List A → List A
+  | A f nil := nil
+  | A f (cons x xs) :=
+    ite
+      (List A)
+      (f x)
+      (cons x (filter A f xs))
+      (filter A f xs);
 
-map : (A : Type) → (B : Type) → (A → B) → List A → List B;
-map A B f nil := nil;
-map A B f (cons x xs) := cons (f x) (map A B f xs);
+map : (A : Type) → (B : Type) → (A → B) → List A → List B
+  | A B f nil := nil
+  | A B f (cons x xs) := cons (f x) (map A B f xs);
 
-zip :
-  (A : Type)
+zip
+  : (A : Type)
     → (B : Type)
     → List A
     → List B
-    → List (Pair A B);
-zip A B nil _ := nil;
-zip A B _ nil := nil;
-zip A B (cons a as) (cons b bs) := nil;
+    → List (Pair A B)
+  | A B nil _ := nil
+  | A B _ nil := nil
+  | A B (cons a as) (cons b bs) := nil;
 
-zipWith :
-  (A : Type)
+zipWith
+  : (A : Type)
     → (B : Type)
     → (C : Type)
     → (A → B → C)
     → List A
     → List B
-    → List C;
-zipWith A B C f nil _ := nil;
-zipWith A B C f _ nil := nil;
-zipWith A B C f (cons a as) (cons b bs) :=
-  cons (f a b) (zipWith A B C f as bs);
+    → List C
+  | A B C f nil _ := nil
+  | A B C f _ nil := nil
+  | A B C f (cons a as) (cons b bs) :=
+    cons (f a b) (zipWith A B C f as bs);
 
-rankn : ((A : Type) → A → A) → Bool → Nat → Pair Bool Nat;
-rankn f b n := mkPair (f Bool b) (f Nat n);
+rankn : ((A : Type) → A → A) → Bool → Nat → Pair Bool Nat
+  | f b n := mkPair (f Bool b) (f Nat n);
 
 -- currying
-trankn : Pair Bool Nat;
-trankn := rankn id false zero;
+trankn : Pair Bool Nat := rankn id false zero;
 
-l1 : List Nat;
-l1 := cons zero nil;
+l1 : List Nat := cons zero nil;
 
-pairEval : (A : Type) → (B : Type) → Pair (A → B) A → B;
-pairEval _ _ (mkPair f x) := f x;
+pairEval : (A : Type) → (B : Type) → Pair (A → B) A → B
+  | _ _ (mkPair f x) := f x;
 
-main : Nat;
-main :=
+main : Nat :=
   headDef
     Nat
     (pairEval Nat Nat (mkPair (add zero) zero))

tests/positive/PolymorphismHoles.juvix

@@ -15,94 +15,90 @@ type Bool :=
   | false : Bool
   | true : Bool;
 
-id : (A : Type) → A → A;
-id _ a := a;
+id : (A : Type) → A → A
+  | _ a := a;
 
 terminating
-undefined : (A : Type) → A;
-undefined A := undefined A;
+undefined : (A : Type) → A
+  | A := undefined A;
 
-add : Nat → Nat → Nat;
-add zero b := b;
-add (suc a) b := suc (add a b);
+add : Nat → Nat → Nat
+  | zero b := b
+  | (suc a) b := suc (add a b);
 
-fst : (A : Type) → (B : Type) → Pair A B → A;
-fst _ _ (mkPair a b) := a;
+fst : (A : Type) → (B : Type) → Pair A B → A
+  | _ _ (mkPair a b) := a;
 
-p : Pair Bool Bool;
-p := mkPair true false;
+p : Pair Bool Bool := mkPair true false;
 
-swap : (A : Type) → (B : Type) → Pair A B → Pair B A;
-swap A B (mkPair a b) := mkPair b a;
+swap : (A : Type) → (B : Type) → Pair A B → Pair B A
+  | A B (mkPair a b) := mkPair b a;
 
-curry :
-  (A : Type)
+curry
+  : (A : Type)
     → (B : Type)
     → (C : Type)
     → (Pair A B → C)
     → A
     → B
-    → C;
-curry A B C f a b := f (mkPair a b);
+    → C
+  | A B C f a b := f (mkPair a b);
 
-ap : (A : Type) → (B : Type) → (A → B) → A → B;
-ap A B f a := f a;
+ap : (A : Type) → (B : Type) → (A → B) → A → B
+  | A B f a := f a;
 
-headDef : (A : Type) → A → List A → A;
-headDef _ d nil := d;
-headDef A _ (cons h _) := h;
+headDef : (A : Type) → A → List A → A
+  | _ d nil := d
+  | A _ (cons h _) := h;
 
-ite : (A : Type) → Bool → A → A → A;
-ite _ true tt _ := tt;
-ite _ false _ ff := ff;
+ite : (A : Type) → Bool → A → A → A
+  | _ true tt _ := tt
+  | _ false _ ff := ff;
 
-filter : (A : Type) → (A → Bool) → List A → List A;
-filter _ f nil := nil;
-filter _ f (cons x xs) :=
-  ite _ (f x) (cons x (filter _ f xs)) (filter _ f xs);
+filter : (A : Type) → (A → Bool) → List A → List A
+  | _ f nil := nil
+  | _ f (cons x xs) :=
+    ite _ (f x) (cons x (filter _ f xs)) (filter _ f xs);
 
-map : (A : Type) → (B : Type) → (A → B) → List _ → List _;
-map _ _ f nil := nil;
-map _ _ f (cons x xs) := cons (f x) (map _ _ f xs);
+map : (A : Type) → (B : Type) → (A → B) → List _ → List _
+  | _ _ f nil := nil
+  | _ _ f (cons x xs) := cons (f x) (map _ _ f xs);
 
-zip :
-  (A : Type)
+zip
+  : (A : Type)
     → (B : Type)
     → List A
     → List B
-    → List (Pair A B);
-zip A _ nil _ := nil;
-zip _ _ _ nil := nil;
-zip _ _ (cons a as) (cons b bs) := nil;
+    → List (Pair A B)
+  | A _ nil _ := nil
+  | _ _ _ nil := nil
+  | _ _ (cons a as) (cons b bs) := nil;
 
-zipWith :
-  (A : Type)
+zipWith
+  : (A : Type)
     → (B : Type)
     → (C : Type)
     → (A → B → C)
     → List A
     → List B
-    → List C;
-zipWith _ _ C f nil _ := nil;
-zipWith _ _ C f _ nil := nil;
-zipWith _ _ _ f (cons a as) (cons b bs) :=
-  cons (f a b) (zipWith _ _ _ f as bs);
+    → List C
+  | _ _ C f nil _ := nil
+  | _ _ C f _ nil := nil
+  | _ _ _ f (cons a as) (cons b bs) :=
+    cons (f a b) (zipWith _ _ _ f as bs);
 
-rankn : ((A : Type) → A → A) → Bool → Nat → Pair Bool Nat;
-rankn f b n := mkPair (f _ b) (f _ n);
+rankn : ((A : Type) → A → A) → Bool → Nat → Pair Bool Nat
+  | f b n := mkPair (f _ b) (f _ n);
 
 -- currying
-trankn : Pair Bool Nat;
-trankn := rankn id false zero;
+trankn : Pair Bool Nat := rankn id false zero;
 
-l1 : List Nat;
-l1 := cons zero nil;
+l1 : List Nat := cons zero nil;
 
-pairEval : (A : Type) → (B : Type) → Pair (A → B) A → B;
-pairEval _ _ (mkPair f x) := f x;
+pairEval : (A : Type) → (B : Type) → Pair (A → B) A → B
+  | _ _ (mkPair f x) := f x;
 
-main : Nat;
-main :=
+main : Nat :=
   headDef
     _
     (pairEval _ _ (mkPair (add zero) zero))

tests/positive/Pragmas.juvix

@@ -11,12 +11,12 @@ axiom a : Nat;
   unroll: 100
   inline: false
 #-}
-f : Nat → Nat;
-f x := x;
+f : Nat → Nat
+  | x := x;
 
 {-# inline: true #-}
-g : Nat → Nat;
-g x := suc x;
+g : Nat → Nat
+  | x := suc x;
 
 {-
 Multiline highlighting
@@ -25,10 +25,9 @@ Multiline highlighting
 --- Judoc comment 2
 {-# unroll: 0 #-}
 terminating
-h : Nat → Nat;
-h x := x + 5;
+h : Nat → Nat
+  | x := x + 5;
 
 --- Judoc comment
 {-# inline: false, unroll: 10, unknownPragma: tratatata #-}
-main : Nat;
-main := 0;
+main : Nat := 0;

tests/positive/QualifiedConstructor/M.juvix

@@ -15,5 +15,5 @@ end;
 
 open N.O;
 
-fun : T → T;
-fun A := T;
+fun : T → T
+  | A := T;

tests/positive/QualifiedImports/Main.juvix

@@ -9,8 +9,7 @@ axiom a : Nat;
 
 axiom b : Longer.For.No.Reason.Nat;
 
-main : Prelude.Nat;
-main := 123;
+main : Prelude.Nat := 123;
 
 -- Merging imports
 import Stdlib.Data.Nat as X;

tests/positive/Reachability/Data/Bool.juvix

@@ -4,6 +4,6 @@ type Bool :=
   | true : Bool
   | false : Bool;
 
-not : Bool → Bool;
-not true := false;
-not false := true;
+not : Bool → Bool
+  | true := false
+  | false := true;

tests/positive/Reachability/Data/Nat.juvix

@@ -5,11 +5,13 @@ type ℕ :=
   | suc : ℕ → ℕ;
 
 syntax infixl 6 +;
-+ : ℕ → ℕ → ℕ;
-+ zero b := b;
-+ (suc a) b := suc (a + b);
+
++ : ℕ → ℕ → ℕ
+  | zero b := b
+  | (suc a) b := suc (a + b);
 
 syntax infixl 7 *;
-* : ℕ → ℕ → ℕ;
-* zero b := zero;
-* (suc a) b := b + a * b;
+
+* : ℕ → ℕ → ℕ
+  | zero b := zero
+  | (suc a) b := b + a * b;

tests/positive/Reachability/M.juvix

@@ -6,11 +6,11 @@ import Data.Product open;
 import Data.Bool open;
 import Data.Ord open;
 
-f : Bool -> Bool;
-f x := x;
+f : Bool -> Bool
+  | x := x;
 
-g : {A : Type} -> A -> Bool -> Bool;
-g x y := f y;
+g : {A : Type} -> A -> Bool -> Bool
+  | x y := f y;
 
-h : {A : Type} -> A -> Maybe Bool;
-h x := nothing;
+h : {A : Type} -> A -> Maybe Bool
+  | x := nothing;

tests/positive/Reachability/N.juvix

@@ -3,8 +3,8 @@ module N;
 import M open;
 import Stdlib.Prelude open hiding {Unit};
 
-test : {A : Type} -> A -> A;
-test x := x;
+test : {A : Type} -> A -> A
+  | x := x;
 
 type Unit :=
   | unit : Unit;

tests/positive/Reachability/O.juvix

@@ -3,5 +3,4 @@ module O;
 import M open public;
 import Stdlib.Data.Bool open;
 
-k : Bool;
-k := true;
+k : Bool := true;

tests/positive/StdlibImport/StdlibImport.juvix

@@ -4,8 +4,6 @@ import Stdlib.Prelude open;
 
 import A;
 
-two : Nat;
-two := 1 + 1;
+two : Nat := 1 + 1;
 
-foo : A.Foo;
-foo := A.bar;
+foo : A.Foo := A.bar;