diff --git a/CODING.md b/CODING.md
index 1a6e145e44..694fa26f76 100644
--- a/CODING.md
+++ b/CODING.md
@@ -1,14 +1,22 @@
 # Juvix coding style guidelines for the standard library and Anoma apps
 
+## Definitions
+
+- _enumeration type_ is an inductive type whose all constructors have zero
+  arguments
+
 ## General rules
 
 - always use the formatter
 - don't use unicode, except perhaps for judoc
 - avoid `Pair`
-- prefer enumerations with meaningful names over booleans, e.g., instead of using `Bool` define:
+- prefer enumeration types with meaningful constructor names over booleans,
+  e.g., instead of using `Bool` define:
 
 ```
-type Transferability := Transferable | NonTransferable;
+type Transferability :=
+  | Transferable
+  | NonTransferable;
 ```
 
 ## Imports
@@ -21,11 +29,34 @@ type Transferability := Transferable | NonTransferable;
 
 - types: upper camel case (`Nat`, `PublicKey`)
 - functions, constructors, etc: lower camel case (`tokenLogic`, `transferLogic`)
+  - exception: constructors of enumeration types: upper camel case
+
+```
+type BalanceFactor :=
+  | --- Left child is higher.
+    LeanLeft
+  | --- Equal heights of children.
+    LeanNone
+  | --- Right child is higher.
+    LeanRight;
+
+type Ordering :=
+  | LessThan
+  | Equal
+  | GreaterThan;
+```
+
 - instances: lower camel case with `I` at the end (`instance eqNatI : Eq Nat := ..`)
 - boolean check functions: start with `is` (`isWhatever`)
 - record constructors: `mk` + type name (`mkResource`)
 - meaningful descriptive long names for arguments of public functions, e.g., `element`, `list`, `initialValue`
-  - exception: common abbreviations allowed: `fun`, `acc`
+  - exception: common abbreviations allowed: `fun`, `acc`. `elem`
+  - exception: generic functions whose arguments have no specific meaning, e.g.,
+
+```
+id {A} (x : A) : A := x
+```
+
 - short names like `x` are okay for local definitions
 
 ## Function signatures
@@ -41,6 +72,7 @@ isMember {A} (testEq : A -> A -> Bool) (element : A) : (list : List A) -> Bool
 ## Type variables
 
 - type variables uppercase (upper camel case, like with types)
+- higher-order type variables also upper camel case (`F : Type -> Type`)
 - implicit type variables: use short version `{A}` in function signatures on the left
 - prefer `{A B}` over `{A} {B}` in function signatures
 - meaningful type variable names for more "high-level" functions where this makes sense
@@ -81,6 +113,24 @@ find {A} (predicate : A -> Bool) : (list : List A) -> Maybe A
 - use iterators `for` , `map`, etc., instead of the function application syntax with `fold`, etc.
 - use named application when reasonable
 
+## Type definitions
+
+- use ADT syntax
+- every constructor on a separate line
+- give meaningful names to constructor arguments
+
+Example:
+
+```
+type BinaryTree (A : Type) :=
+  | leaf
+  | node {
+      left : BinaryTree A;
+      element : A;
+      right : BinaryTree A
+    };
+```
+
 ## Documentation
 
 - the documentation string should be an English sentence
diff --git a/cntlines.sh b/cntlines.sh
index 8addd62062..6d7ce0434e 100755
--- a/cntlines.sh
+++ b/cntlines.sh
@@ -45,6 +45,7 @@ FRONT=$((CONCRETE + INTERNAL + BUILTINS + PIPELINE))
 BACK=$((BACKENDC + BACKENDRUST + VAMPIR + NOCK + REG + ASM + TREE + CORE + CASM + CAIRO))
 OTHER=$((APP + STORE + HTML + MARKDOWN + ISABELLE + EXTRA + DATA + PRELUDE))
 TESTS=$(count test/)
+STDLIB=$(count_ext '*.juvix' juvix-stdlib/Stdlib)
 
 TOTAL=$((FRONT+BACK+OTHER+TESTS))
 
@@ -79,5 +80,6 @@ echo "   Extra: $EXTRA LOC"
 echo "   Data: $DATA LOC"
 echo "   Prelude: $PRELUDE LOC"
 echo "Tests: $TESTS LOC"
+echo "Standard library: $STDLIB LOC"
 echo ""
-echo "Total: $TOTAL Haskell LOC + $RUNTIME_C C LOC + $RUNTIME_RUST Rust LOC + $RUNTIME_JVT JuvixTree LOC + $RUNTIME_CASM CASM LOC + $RUNTIME_VAMPIR VampIR LOC"
+echo "Total: $TOTAL Haskell LOC + $RUNTIME_C C LOC + $RUNTIME_RUST Rust LOC + $RUNTIME_JVT JuvixTree LOC + $RUNTIME_CASM CASM LOC + $RUNTIME_VAMPIR VampIR LOC + $STDLIB Juvix LOC"
diff --git a/examples/demo/Demo.juvix b/examples/demo/Demo.juvix
index 0a0dcff0f8..06a4e91fcd 100644
--- a/examples/demo/Demo.juvix
+++ b/examples/demo/Demo.juvix
@@ -3,40 +3,46 @@ module Demo;
 -- standard library prelude
 import Stdlib.Prelude open;
 
-even : Nat → Bool
+even : (n : Nat) -> Bool
   | zero := true
   | (suc zero) := false
   | (suc (suc n)) := even n;
 
-even' : Nat → Bool
-  | n := mod n 2 == 0;
+even' (n : Nat) : Bool := mod n 2 == 0;
 
--- base 2 logarithm rounded down
+--- Returns base 2 logarithm of `n` rounded down
 terminating
-log2 : Nat → Nat
-  | n := ite (n <= 1) 0 (suc (log2 (div n 2)));
+log2 (n : Nat) : Nat :=
+  if
+    | n <= 1 := 0
+    | else := log2 (div n 2) + 1;
 
 type Tree (A : Type) :=
-  | leaf : A → Tree A
-  | node : A → Tree A → Tree A → Tree A;
-
-mirror : {A : Type} → Tree A → Tree A
-  | t@(leaf _) := t
+  | leaf {element : A}
+  | node {
+      element : A;
+      left : Tree A;
+      right : Tree A
+    };
+
+mirror {A} : (tree : Tree A) -> Tree A
+  | tree@(leaf _) := tree
   | (node x l r) := node x (mirror r) (mirror l);
 
 tree : Tree Nat := node 2 (node 3 (leaf 0) (leaf 1)) (leaf 7);
 
-preorder : {A : Type} → Tree A → List A
+preorder : {A : Type} -> Tree A -> List A
   | (leaf x) := x :: nil
   | (node x l r) := x :: nil ++ preorder l ++ preorder r;
 
 terminating
-sort {A} {{Ord A}} : List A → List A
-  | nil := nil
-  | xs@(_ :: nil) := xs
-  | xs := uncurry merge (both sort (splitAt (div (length xs) 2) xs));
+sort {A} {{Ord A}} (list : List A) : List A :=
+  case list of
+    | nil := nil
+    | xs@(_ :: nil) := xs
+    | xs := uncurry merge (both sort (splitAt (div (length xs) 2) xs));
 
-printNatListLn : List Nat → IO
+printNatListLn : (list : List Nat) -> IO
   | nil := printStringLn "nil"
   | (x :: xs) := printNat x >>> printString " :: " >>> printNatListLn xs;
 
diff --git a/examples/midsquare/MidSquareHash.juvix b/examples/midsquare/MidSquareHash.juvix
index 1a50f54f29..eb901557a2 100644
--- a/examples/midsquare/MidSquareHash.juvix
+++ b/examples/midsquare/MidSquareHash.juvix
@@ -6,15 +6,18 @@ module MidSquareHash;
 
 import Stdlib.Prelude open;
 
---- `pow N` is 2 ^ N
-pow : Nat -> Nat
+--- `pow n` is 2 ^ n
+pow : (n : 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
+--- `hash' n x` hashes a number x 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
-  | (suc n@(suc (suc m))) x := ite (x < pow n) (hash' n x) (mod (div (x * x) (pow m)) (pow 6))
+hash' : (n : Nat) -> (x : Nat) -> Nat
+  | (suc n'@(suc (suc m))) x :=
+    if
+      | x < pow n' := hash' n' x
+      | else := mod (div (x * x) (pow m)) (pow 6)
   | _ x := x * x;
 
 hash : Nat -> Nat := hash' 16;
diff --git a/examples/midsquare/MidSquareHashUnrolled.juvix b/examples/midsquare/MidSquareHashUnrolled.juvix
index 0f7927ac09..3493d6fdc7 100644
--- a/examples/midsquare/MidSquareHashUnrolled.juvix
+++ b/examples/midsquare/MidSquareHashUnrolled.juvix
@@ -44,56 +44,78 @@ 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
-  | x := 0;
-
-hash1 : Nat -> Nat
-  | x := x * x;
-
-hash2 : Nat -> Nat
-  | x := x * x;
-
-hash3 : Nat -> Nat
-  | x := x * x;
-
-hash4 : Nat -> Nat
-  | x := ite (x < pow3) (hash3 x) (mod (div (x * x) pow1) pow6);
-
-hash5 : Nat -> Nat
-  | x := ite (x < pow4) (hash4 x) (mod (div (x * x) pow2) pow6);
-
-hash6 : Nat -> Nat
-  | x := ite (x < pow5) (hash5 x) (mod (div (x * x) pow3) pow6);
-
-hash7 : Nat -> Nat
-  | x := ite (x < pow6) (hash6 x) (mod (div (x * x) pow4) pow6);
-
-hash8 : Nat -> Nat
-  | x := ite (x < pow7) (hash7 x) (mod (div (x * x) pow5) pow6);
-
-hash9 : Nat -> Nat
-  | x := ite (x < pow8) (hash8 x) (mod (div (x * x) pow6) pow6);
-
-hash10 : Nat -> Nat
-  | x := ite (x < pow9) (hash9 x) (mod (div (x * x) pow7) pow6);
-
-hash11 : Nat -> Nat
-  | x := ite (x < pow10) (hash10 x) (mod (div (x * x) pow8) pow6);
-
-hash12 : Nat -> Nat
-  | x := ite (x < pow11) (hash11 x) (mod (div (x * x) pow9) pow6);
-
-hash13 : Nat -> Nat
-  | x := ite (x < pow12) (hash12 x) (mod (div (x * x) pow10) pow6);
-
-hash14 : Nat -> Nat
-  | x := ite (x < pow13) (hash13 x) (mod (div (x * x) pow11) pow6);
-
-hash15 : Nat -> Nat
-  | x := ite (x < pow14) (hash14 x) (mod (div (x * x) pow12) pow6);
-
-hash16 : Nat -> Nat
-  | x := ite (x < pow15) (hash15 x) (mod (div (x * x) pow13) pow6);
+hash0 (x : Nat) : Nat := 0;
+
+hash1 (x : Nat) : Nat := x * x;
+
+hash2 (x : Nat) : Nat := x * x;
+
+hash3 (x : Nat) : Nat := x * x;
+
+hash4 (x : Nat) : Nat :=
+  if
+    | x < pow3 := hash3 x
+    | else := mod (div (x * x) pow1) pow6;
+
+hash5 (x : Nat) : Nat :=
+  if
+    | x < pow4 := hash4 x
+    | else := mod (div (x * x) pow2) pow6;
+
+hash6 (x : Nat) : Nat :=
+  if
+    | x < pow5 := hash5 x
+    | else := mod (div (x * x) pow3) pow6;
+
+hash7 (x : Nat) : Nat :=
+  if
+    | x < pow6 := hash6 x
+    | else := mod (div (x * x) pow4) pow6;
+
+hash8 (x : Nat) : Nat :=
+  if
+    | x < pow7 := hash7 x
+    | else := mod (div (x * x) pow5) pow6;
+
+hash9 (x : Nat) : Nat :=
+  if
+    | x < pow8 := hash8 x
+    | else := mod (div (x * x) pow6) pow6;
+
+hash10 (x : Nat) : Nat :=
+  if
+    | x < pow9 := hash9 x
+    | else := mod (div (x * x) pow7) pow6;
+
+hash11 (x : Nat) : Nat :=
+  if
+    | x < pow10 := hash10 x
+    | else := mod (div (x * x) pow8) pow6;
+
+hash12 (x : Nat) : Nat :=
+  if
+    | x < pow11 := hash11 x
+    | else := mod (div (x * x) pow9) pow6;
+
+hash13 (x : Nat) : Nat :=
+  if
+    | x < pow12 := hash12 x
+    | else := mod (div (x * x) pow10) pow6;
+
+hash14 (x : Nat) : Nat :=
+  if
+    | x < pow13 := hash13 x
+    | else := mod (div (x * x) pow11) pow6;
+
+hash15 (x : Nat) : Nat :=
+  if
+    | x < pow14 := hash14 x
+    | else := mod (div (x * x) pow12) pow6;
+
+hash16 (x : Nat) : Nat :=
+  if
+    | x < pow15 := hash15 x
+    | else := mod (div (x * x) pow13) pow6;
 
 hash : Nat -> Nat := hash16;
 
diff --git a/examples/milestone/Bank/Bank.juvix b/examples/milestone/Bank/Bank.juvix
index 876e967d57..ad1f7b128b 100644
--- a/examples/milestone/Bank/Bank.juvix
+++ b/examples/milestone/Bank/Bank.juvix
@@ -12,41 +12,35 @@ Address : Type := Nat;
 
 bankAddress : Address := 1234;
 
-module Token;
-  type Token :=
-    --- Arguments are: owner, gates, amount.
-    mkToken : Address -> Nat -> Nat -> Token;
-
-  --- Retrieves the owner from a ;Token;
-  getOwner : Token -> Address
-    | (mkToken o _ _) := o;
-
-  --- Retrieves the amount from a ;Token;
-  getAmount : Token -> Nat
-    | (mkToken _ _ a) := a;
-
-  --- Retrieves the gates from a ;Token;
-  getGates : Token -> Nat
-    | (mkToken _ g _) := g;
-end;
-
-open Token;
+type Token :=
+  --- Arguments are: owner, gates, amount.
+  mkToken {
+    owner : Address;
+    gates : Nat;
+    amount : Nat
+  };
 
 --- This module defines the type for balances and its associated operations.
 module Balances;
   Balances : Type := List (Pair Field Nat);
 
   --- Increments the amount associated with a certain ;Field;.
-  increment : Field -> Nat -> Balances -> Balances
-    | f n nil := (f, n) :: nil
-    | f n ((b, bn) :: bs) := ite (f == b) ((b, bn + n) :: bs) ((b, bn) :: increment f n bs);
+  increment (fld : Field) (n : Nat) : (balances : Balances) -> Balances
+    | nil := (fld, n) :: nil
+    | ((b, bn) :: bs) :=
+      if
+        | fld == b := (b, bn + n) :: bs
+        | else := (b, bn) :: increment fld 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
-    | _ _ nil := nil
-    | f n ((b, bn) :: bs) := ite (f == b) ((b, sub bn n) :: bs) ((b, bn) :: decrement f n bs);
+  decrement (fld : Field) (n : Nat) : (balances : Balances) -> Balances
+    | nil := nil
+    | ((b, bn) :: bs) :=
+      if
+        | fld == b := (b, sub bn n) :: bs
+        | else := (b, bn) :: decrement fld n bs;
 
   emtpyBalances : Balances := nil;
 
@@ -63,12 +57,11 @@ 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
-  | principal rate periods :=
-    let
-      amount : Nat := principal;
-      incrAmount (a : Nat) : Nat := div (a * rate) 10000;
-    in iterate (min 100 periods) incrAmount amount;
+calculateInterest (principal rate periods : Nat) : Nat :=
+  let
+    amount : Nat := principal;
+    incrAmount (a : Nat) : Nat := div (a * rate) 10000;
+  in iterate (min 100 periods) incrAmount amount;
 
 --- Returns a new ;Token;. Arguments are:
 ---
@@ -77,15 +70,15 @@ calculateInterest : Nat -> Nat -> Nat -> Nat
 --- `amount`: The amount of  tokens to issue
 ---
 --- `caller`: Who is creating the transaction. It must be the bank.
-issue : Address -> Address -> Nat -> Token
-  | caller owner amount := assert (caller == bankAddress) >-> mkToken owner 0 amount;
+issue (caller owner : Address) (amount : 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 :=
   let
-    difference : Nat := sub (getAmount token) amount;
-    remaining : Token := mkToken (getOwner token) (getGates token) difference;
-    hash : Field := hashAddress (getOwner token);
+    difference : Nat := sub (Token.amount token) amount;
+    remaining : Token := mkToken (Token.owner token) (Token.gates token) difference;
+    hash : Field := hashAddress (Token.owner token);
     bal' : Balances := increment hash amount bal;
   in runOnChain (commitBalances bal') remaining;
 
diff --git a/examples/milestone/Collatz/Collatz.juvix b/examples/milestone/Collatz/Collatz.juvix
index eed4d4ba11..8cc560a0ab 100644
--- a/examples/milestone/Collatz/Collatz.juvix
+++ b/examples/milestone/Collatz/Collatz.juvix
@@ -2,17 +2,22 @@ module Collatz;
 
 import Stdlib.Prelude open;
 
-collatzNext (n : Nat) : Nat := ite (mod n 2 == 0) (div n 2) (3 * n + 1);
+collatzNext (n : Nat) : Nat :=
+  if
+    | mod n 2 == 0 := div n 2
+    | else := 3 * n + 1;
 
-collatz : Nat → Nat
-  | zero := zero
-  | (suc zero) := suc zero
-  | n := collatzNext n;
+collatz (n : Nat) : Nat :=
+  case n of
+    | zero := zero
+    | suc zero := suc zero
+    | n := collatzNext n;
 
 terminating
-run (f : Nat → Nat) : Nat → IO
-  | (suc zero) := printNatLn 1 >>> printStringLn "Finished!"
-  | n := printNatLn n >>> run f (f n);
+run (f : Nat -> Nat) (n : Nat) : IO :=
+  case n of
+    | suc zero := printNatLn 1 >>> printStringLn "Finished!"
+    | n := printNatLn n >>> run f (f n);
 
 welcome : String := "Collatz calculator\n------------------\n\nType a number then ENTER";
 
diff --git a/examples/milestone/Fibonacci/Fibonacci.juvix b/examples/milestone/Fibonacci/Fibonacci.juvix
index 3b5ebbd78b..d4b63acedf 100644
--- a/examples/milestone/Fibonacci/Fibonacci.juvix
+++ b/examples/milestone/Fibonacci/Fibonacci.juvix
@@ -2,7 +2,7 @@ module Fibonacci;
 
 import Stdlib.Prelude open;
 
-fib : Nat → Nat → Nat → Nat
+fib : (n : Nat) -> (x1 : Nat) -> (x2 : Nat) -> Nat
   | zero x1 _ := x1
   | (suc n) x1 x2 := fib n x2 (x1 + x2);
 
diff --git a/examples/milestone/Hanoi/Hanoi.juvix b/examples/milestone/Hanoi/Hanoi.juvix
index 355c64f1eb..c641593b4d 100644
--- a/examples/milestone/Hanoi/Hanoi.juvix
+++ b/examples/milestone/Hanoi/Hanoi.juvix
@@ -16,39 +16,40 @@ import Stdlib.Prelude open;
 
 --- Concatenates a list of strings
 --- ;concat (("a" :: nil) :: "b" :: nil); evaluates to ;"a" :: "b" :: nil;
-concat : List String → String := foldl (++str) "";
+concat (list : List String) : String := foldl (++str) "" list;
 
-intercalate : String → List String → String
-  | sep xs := concat (intersperse sep xs);
+intercalate (sep : String) (xs : List String) : String := concat (intersperse sep xs);
 
 --- Produce a singleton List
-singleton : {A : Type} → A → List A
-  | a := a :: nil;
+singleton {A} (a : A) : List A := a :: nil;
 
 --- Produce a ;String; representation of a ;List Nat;
-showList : List Nat → String
-  | xs := "[" ++str intercalate "," (map natToString xs) ++str "]";
+showList (xs : List Nat) : String := "[" ++str intercalate "," (map natToString xs) ++str "]";
 
 --- A Peg represents a peg in the towers of Hanoi game
 type Peg :=
-  | left : Peg
-  | middle : Peg
-  | right : Peg;
+  | left
+  | middle
+  | right;
 
-showPeg : Peg → String
+showPeg : Peg -> String
   | left := "left"
   | middle := "middle"
   | right := "right";
 
 --- A Move represents a move between pegs
-type Move := move : Peg → Peg → Move;
+type Move :=
+  mkMove {
+    from : Peg;
+    to : Peg
+  };
 
-showMove : Move → String
-  | (move from to) := showPeg from ++str " -> " ++str showPeg to;
+showMove (move : Move) : String :=
+  showPeg (Move.from move) ++str " -> " ++str showPeg (Move.to move);
 
 --- Produce a list of ;Move;s that solves the towers of Hanoi game
-hanoi : Nat → Peg → Peg → Peg → List Move
+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;
+  | (suc n) p1 p2 p3 := hanoi n p1 p3 p2 ++ singleton (mkMove p1 p2) ++ hanoi n p3 p2 p1;
 
 main : IO := printStringLn (unlines (map showMove (hanoi 5 left middle right)));
diff --git a/examples/milestone/PascalsTriangle/PascalsTriangle.juvix b/examples/milestone/PascalsTriangle/PascalsTriangle.juvix
index a940b4df6d..be712f7f9c 100644
--- a/examples/milestone/PascalsTriangle/PascalsTriangle.juvix
+++ b/examples/milestone/PascalsTriangle/PascalsTriangle.juvix
@@ -7,16 +7,16 @@ module PascalsTriangle;
 import Stdlib.Prelude open;
 
 --- Return a list of repeated applications of a given function
-scanIterate {A} : Nat → (A → A) → A → List A
+scanIterate {A} : (n : Nat) -> (fun : A -> A) -> (value : A) -> List A
   | zero _ _ := nil
   | (suc n) f a := a :: scanIterate n f (f a);
 
 --- Produce a singleton List
-singleton {A} (a : A) : List A := a :: nil;
+singleton {A} (value : A) : List A := value :: nil;
 
 --- Concatenates a list of strings
 --- ;concat (("a" :: nil) :: "b" :: nil); evaluates to ;"a" :: "b" :: nil;
-concat : List String → String := foldl (++str) "";
+concat (list : List String) : String := foldl (++str) "" list;
 
 intercalate (sep : String) (xs : List String) : String := concat (intersperse sep xs);
 
diff --git a/examples/milestone/TicTacToe/CLI/TicTacToe.juvix b/examples/milestone/TicTacToe/CLI/TicTacToe.juvix
index ca208bb7d1..5bd48fefe9 100644
--- a/examples/milestone/TicTacToe/CLI/TicTacToe.juvix
+++ b/examples/milestone/TicTacToe/CLI/TicTacToe.juvix
@@ -9,20 +9,28 @@ import Stdlib.Prelude open;
 import Logic.Game open;
 
 --- A ;String; that prompts the user for their input
-prompt (x : GameState) : String :=
-  "\n" ++str showGameState x ++str "\nPlayer " ++str showSymbol (player x) ++str ": ";
+prompt (state : GameState) : String :=
+  "\n"
+    ++str showGameState state
+    ++str "\nPlayer "
+    ++str showSymbol (GameState.player state)
+    ++str ": ";
 
-nextMove (s : GameState) : String → GameState := stringToNat >> validMove >> flip playMove s;
+nextMove (state : GameState) (string : String) : GameState :=
+  string |> stringToNat |> validMove |> flip playMove state;
 
 --- Main loop
 terminating
-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);
+run (state : GameState) : IO :=
+  case GameState.error state of
+    | terminate msg :=
+      printStringLn
+        ("\n" ++str showGameState state@GameState{error := noError} ++str "\n" ++str msg)
+    | continue msg :=
+      let
+        state' := state@GameState{error := noError};
+      in printString (msg ++str prompt state') >>> readLn (nextMove state' >> run)
+    | _ := printString (prompt state) >>> readLn (nextMove state >> run);
 
 --- The welcome message
 welcome : String := "MiniTicTacToe\n-------------\n\nType a number then ENTER to make a move";
diff --git a/examples/milestone/TicTacToe/Logic/Board.juvix b/examples/milestone/TicTacToe/Logic/Board.juvix
index 5f269f4835..28cfa06674 100644
--- a/examples/milestone/TicTacToe/Logic/Board.juvix
+++ b/examples/milestone/TicTacToe/Logic/Board.juvix
@@ -7,30 +7,32 @@ import Logic.Symbol open public;
 import Logic.Extra open;
 
 --- A 3x3 grid of ;Square;s
-type Board := board : List (List Square) → Board;
+type Board := mkBoard {squares : List (List Square)};
 
 --- Returns the list of numbers corresponding to the empty ;Square;s
-possibleMoves : List Square → List Nat
+possibleMoves : (list : 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
-  | (a :: b :: c :: nil) := ==Square a b && ==Square b c
-  | _ := failwith "full";
+full (list : List Square) : Bool :=
+  case list of
+    | a :: b :: c :: nil := a == b && b == c
+    | _ := failwith "full";
 
-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
-  | _ := failwith "diagonals";
+diagonals (squares : List (List Square)) : List (List Square) :=
+  case squares of
+    | (a1 :: _ :: b1 :: nil) :: (_ :: c :: _ :: nil) :: (b2 :: _ :: a2 :: nil) :: nil :=
+      (a1 :: c :: a2 :: nil) :: (b1 :: c :: b2 :: nil) :: nil
+    | _ := failwith "diagonals";
 
-columns : List (List Square) → List (List Square) := transpose;
+columns (squares : List (List Square)) : List (List Square) := transpose squares;
 
-rows : List (List Square) → List (List Square) := id;
+rows (squares : List (List Square)) : List (List Square) := squares;
 
 --- Textual representation of a ;List Square;
 showRow (xs : List Square) : String := concat (surround "|" (map showSquare xs));
 
-showBoard : Board → String
-  | (board squares) := unlines (surround "+---+---+---+" (map showRow squares));
+showBoard (board : Board) : String :=
+  unlines (surround "+---+---+---+" (map showRow (Board.squares board)));
diff --git a/examples/milestone/TicTacToe/Logic/Extra.juvix b/examples/milestone/TicTacToe/Logic/Extra.juvix
index daa07ccd3e..4fd9848ad2 100644
--- a/examples/milestone/TicTacToe/Logic/Extra.juvix
+++ b/examples/milestone/TicTacToe/Logic/Extra.juvix
@@ -5,7 +5,7 @@ import Stdlib.Prelude open;
 
 --- Concatenates a list of strings
 --- ;concat (("a" :: nil) :: "b" :: nil); evaluates to ;"a" :: "b" :: nil;
-concat : List String → String := foldl (++str) "";
+concat (list : List String) : String := foldl (++str) "" list;
 
 --- It inserts the first ;String; at the beginning, in between, and at the end of the second list
 surround (x : String) (xs : List String) : List String := (x :: intersperse x xs) ++ x :: nil;
diff --git a/examples/milestone/TicTacToe/Logic/Game.juvix b/examples/milestone/TicTacToe/Logic/Game.juvix
index 3e7c8d42ca..b4a64eaaf8 100644
--- a/examples/milestone/TicTacToe/Logic/Game.juvix
+++ b/examples/milestone/TicTacToe/Logic/Game.juvix
@@ -10,21 +10,32 @@ import Logic.Board open public;
 import Logic.GameState open public;
 
 --- Checks if we reached the end of the game.
-checkState : GameState → GameState
-  | (state b p e) :=
-    ite
-      (won (state b p e))
-      (state b p (terminate ("Player " ++str showSymbol (switch p) ++str " wins!")))
-      (ite (draw (state b p e)) (state b p (terminate "It's a draw!")) (state b p e));
+checkState (state : GameState) : GameState :=
+  if
+    | won state :=
+      state@GameState{error := terminate
+        ("Player " ++str showSymbol (switch (GameState.player state)) ++str " wins!")}
+    | draw state := state@GameState{error := terminate "It's a draw!"}
+    | else := state;
 
 --- Given a player attempted move, updates the state accordingly.
-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) :=
-    ite
-      (not (elem (==) k (possibleMoves (flatten s))))
-      (state (board s) player (continue "\nThe square is already occupied, try again\n"))
-      (checkState (state (board (map (map (replace player k)) s)) (switch player) noError));
+playMove (attemptedMove : Maybe Nat) (state : GameState) : GameState :=
+  case attemptedMove of
+    | nothing := state@GameState{error := continue "\nInvalid number, try again\n"}
+    | just k :=
+      let
+        squares := Board.squares (GameState.board state);
+        player' := GameState.player state;
+      in if
+        | not (isMember k (possibleMoves (flatten squares))) :=
+          state@GameState{error := continue "\nThe square is already occupied, try again\n"}
+        | else :=
+          checkState
+            mkGameState@{
+              board := mkBoard (map (map (replace player' k)) squares);
+              player := switch player';
+              error := noError
+            };
 
 --- Returns ;just; if the given ;Nat; is in range of 1..9
 validMove (n : Nat) : Maybe Nat := ite (n <= 9 && n >= 1) (just n) nothing;
diff --git a/examples/milestone/TicTacToe/Logic/GameState.juvix b/examples/milestone/TicTacToe/Logic/GameState.juvix
index 4009c8ebb0..24853ef0a4 100644
--- a/examples/milestone/TicTacToe/Logic/GameState.juvix
+++ b/examples/milestone/TicTacToe/Logic/GameState.juvix
@@ -12,30 +12,36 @@ type Error :=
   | --- a fatal occurred
     terminate : String → Error;
 
-type GameState := state : Board → Symbol → Error → GameState;
+type GameState :=
+  mkGameState {
+    board : Board;
+    player : Symbol;
+    error : Error
+  };
 
 --- Textual representation of a ;GameState;
-showGameState : GameState → String
-  | (state b _ _) := showBoard b;
-
---- Projects the player
-player : GameState → Symbol
-  | (state _ p _) := p;
+showGameState (state : GameState) : String := showBoard (GameState.board state);
 
 --- initial ;GameState;
 beginState : GameState :=
-  state
-    (board
-      (map
-        (map empty)
-        ((1 :: 2 :: 3 :: nil) :: (4 :: 5 :: 6 :: nil) :: (7 :: 8 :: 9 :: nil) :: nil)))
-    X
-    noError;
+  mkGameState@{
+    board :=
+      mkBoard
+        (map
+          (map empty)
+          ((1 :: 2 :: 3 :: nil) :: (4 :: 5 :: 6 :: nil) :: (7 :: 8 :: 9 :: nil) :: nil));
+    player := X;
+    error := noError
+  };
 
 --- ;true; if some player has won the game
-won : GameState → Bool
-  | (state (board squares) _ _) := any full (diagonals squares ++ rows squares ++ columns squares);
+won (state : GameState) : Bool :=
+  let
+    squares := Board.squares (GameState.board state);
+  in any full (diagonals squares ++ rows squares ++ columns squares);
 
 --- ;true; if there is a draw
-draw : GameState → Bool
-  | (state (board squares) _ _) := null (possibleMoves (flatten squares));
+draw (state : GameState) : Bool :=
+  let
+    squares := Board.squares (GameState.board state);
+  in null (possibleMoves (flatten squares));
diff --git a/examples/milestone/TicTacToe/Logic/Square.juvix b/examples/milestone/TicTacToe/Logic/Square.juvix
index b60017e5b6..46c8ecea20 100644
--- a/examples/milestone/TicTacToe/Logic/Square.juvix
+++ b/examples/milestone/TicTacToe/Logic/Square.juvix
@@ -7,21 +7,30 @@ import Logic.Extra open;
 --- A square is each of the holes in a board
 type Square :=
   | --- An empty square has a ;Nat; that uniquely identifies it
-    empty : Nat → Square
+    empty {id : Nat}
   | --- An occupied square has a ;Symbol; in it
-    occupied : Symbol → Square;
+    occupied {player : Symbol};
 
---- Equality for ;Square;s
-==Square : Square → Square → Bool
-  | (empty m) (empty n) := m == n
-  | (occupied s) (occupied t) := ==Symbol s t
-  | _ _ := false;
+instance
+eqSquareI : Eq Square :=
+  mkEq@{
+    eq (square1 square2 : Square) : Bool :=
+      case square1, square2 of
+        | empty m, empty n := m == n
+        | occupied s, occupied t := s == t
+        | _, _ := false
+  };
 
 --- Textual representation of a ;Square;
-showSquare : Square → String
-  | (empty n) := " " ++str natToString n ++str " "
-  | (occupied s) := " " ++str showSymbol s ++str " ";
+showSquare (square : Square) : String :=
+  case square of
+    | empty n := " " ++str natToString n ++str " "
+    | occupied s := " " ++str showSymbol s ++str " ";
 
-replace (player : Symbol) (k : Nat) : Square → Square
-  | (empty n) := ite (n == k) (occupied player) (empty n)
-  | s := s;
+replace (player : Symbol) (k : Nat) (square : Square) : Square :=
+  case square of
+    | empty n :=
+      if
+        | n == k := occupied player
+        | else := empty n
+    | s := s;
diff --git a/examples/milestone/TicTacToe/Logic/Symbol.juvix b/examples/milestone/TicTacToe/Logic/Symbol.juvix
index 302849fb84..2a8c104cf9 100644
--- a/examples/milestone/TicTacToe/Logic/Symbol.juvix
+++ b/examples/milestone/TicTacToe/Logic/Symbol.juvix
@@ -6,22 +6,28 @@ import Stdlib.Prelude open;
 --- A symbol represents a token that can be placed in a square
 type Symbol :=
   | --- The circle token
-    O : Symbol
+    O
   | --- The cross token
-    X : Symbol;
+    X;
 
---- Equality for ;Symbol;s
-==Symbol : Symbol → Symbol → Bool
-  | O O := true
-  | X X := true
-  | _ _ := false;
+instance
+eqSymbolI : Eq Symbol :=
+  mkEq@{
+    eq (sym1 sym2 : Symbol) : Bool :=
+      case sym1, sym2 of
+        | O, O := true
+        | X, X := true
+        | _, _ := false
+  };
 
 --- Turns ;O; into ;X; and ;X; into ;O;
-switch : Symbol → Symbol
-  | O := X
-  | X := O;
+switch (sym : Symbol) : Symbol :=
+  case sym of
+    | O := X
+    | X := O;
 
 --- Textual representation of a ;Symbol;
-showSymbol : Symbol → String
-  | O := "O"
-  | X := "X";
+showSymbol (sym : Symbol) : String :=
+  case sym of
+    | O := "O"
+    | X := "X";
diff --git a/examples/milestone/TicTacToe/TicTacToe.juvix b/examples/milestone/TicTacToe/TicTacToe.juvix
index c3d4af5066..0c353aa0e5 100644
--- a/examples/milestone/TicTacToe/TicTacToe.juvix
+++ b/examples/milestone/TicTacToe/TicTacToe.juvix
@@ -1,4 +1,3 @@
 module TicTacToe;
 
 import CLI.TicTacToe;
-import CLI.TicTacToe;
diff --git a/include/package-base/Juvix/Builtin/V1/List.juvix b/include/package-base/Juvix/Builtin/V1/List.juvix
index f688590e42..47708737ec 100644
--- a/include/package-base/Juvix/Builtin/V1/List.juvix
+++ b/include/package-base/Juvix/Builtin/V1/List.juvix
@@ -5,8 +5,8 @@ import Juvix.Builtin.V1.Fixity open;
 syntax operator :: cons;
 --- Inductive list.
 builtin list
-type List (a : Type) :=
+type List (A : Type) :=
   | --- The empty list
     nil
   | --- An element followed by a list
-    :: a (List a);
+    :: A (List A);
diff --git a/include/package-base/Juvix/Builtin/V1/Nat/Base.juvix b/include/package-base/Juvix/Builtin/V1/Nat/Base.juvix
index d0484b9b4c..496febcf60 100644
--- a/include/package-base/Juvix/Builtin/V1/Nat/Base.juvix
+++ b/include/package-base/Juvix/Builtin/V1/Nat/Base.juvix
@@ -12,7 +12,7 @@ syntax operator + additive;
 
 --- Addition for ;Nat;s.
 builtin nat-plus
-+ : Nat → Nat → Nat
++ : Nat -> Nat -> Nat
   | zero b := b
   | (suc a) b := suc (a + b);
 
@@ -20,13 +20,13 @@ syntax operator * multiplicative;
 
 --- Multiplication for ;Nat;s.
 builtin nat-mul
-* : Nat → Nat → Nat
+* : Nat -> Nat -> Nat
   | zero _ := zero
   | (suc a) b := b + a * b;
 
 --- Truncated subtraction for ;Nat;s.
 builtin nat-sub
-sub : Nat → Nat → Nat
+sub : Nat -> Nat -> Nat
   | zero _ := zero
   | n zero := n
   | (suc n) (suc m) := sub n m;
@@ -34,7 +34,7 @@ sub : Nat → Nat → Nat
 --- Division for ;Nat;s. Returns ;zero; if the first element is ;zero;.
 builtin nat-udiv
 terminating
-udiv : Nat → Nat → Nat
+udiv : Nat -> Nat -> Nat
   | zero _ := zero
   | n m := suc (udiv (sub n m) m);
 
diff --git a/juvix-stdlib b/juvix-stdlib
index a38bcd2d29..ff351799c0 160000
--- a/juvix-stdlib
+++ b/juvix-stdlib
@@ -1 +1 @@
-Subproject commit a38bcd2d2935b379d606591ac78eaa2cd0cf24b7
+Subproject commit ff351799c068e7b3e23dd903547d228dc30aff5e
diff --git a/src/Juvix/Compiler/Concrete/Data/NameSpace.hs b/src/Juvix/Compiler/Concrete/Data/NameSpace.hs
index fa9a6c3066..35cc422e72 100644
--- a/src/Juvix/Compiler/Concrete/Data/NameSpace.hs
+++ b/src/Juvix/Compiler/Concrete/Data/NameSpace.hs
@@ -61,7 +61,5 @@ resolveNameSpaceEntry = case sing :: SNameSpace ns of
     resolveFixitySymbolEntry (FixitySymbolEntry n1) (FixitySymbolEntry n2) = FixitySymbolEntry (resolveName n1 n2)
 
     resolveName :: S.Name -> S.Name -> S.Name
-    resolveName n1 n2
-      | n1 ^. S.nameId == n2 ^. S.nameId =
-          over S.nameVisibilityAnn (resolveVisibility (n2 ^. S.nameVisibilityAnn)) n1
-      | otherwise = impossible
+    resolveName n1 n2 =
+      over S.nameVisibilityAnn (resolveVisibility (n2 ^. S.nameVisibilityAnn)) n1
diff --git a/src/Juvix/Data/CodeAnn.hs b/src/Juvix/Data/CodeAnn.hs
index 01225bc041..c2256fe336 100644
--- a/src/Juvix/Data/CodeAnn.hs
+++ b/src/Juvix/Data/CodeAnn.hs
@@ -104,7 +104,7 @@ kwInclude :: Doc Ann
 kwInclude = keyword Str.include
 
 kwArrow :: Doc Ann
-kwArrow = keyword Str.toUnicode
+kwArrow = keyword Str.toAscii
 
 kwMapsto :: Doc Ann
 kwMapsto = keyword Str.mapstoUnicode
diff --git a/src/Juvix/Parser/Lexer.hs b/src/Juvix/Parser/Lexer.hs
index c1268e47a6..518f96c995 100644
--- a/src/Juvix/Parser/Lexer.hs
+++ b/src/Juvix/Parser/Lexer.hs
@@ -119,7 +119,7 @@ space' special =
                   | otherwise -> return (acc <> pack txt)
 
 integerWithBase' :: ParsecS r (WithLoc IntegerWithBase)
-integerWithBase' = withLoc $ do
+integerWithBase' = P.try $ withLoc $ do
   minus <- optional (char '-')
   b <- integerBase'
   num :: Integer <- case b of
diff --git a/tests/Anoma/Compilation/positive/test069.juvix b/tests/Anoma/Compilation/positive/test069.juvix
index 98d49c65fe..3500b88af9 100644
--- a/tests/Anoma/Compilation/positive/test069.juvix
+++ b/tests/Anoma/Compilation/positive/test069.juvix
@@ -5,7 +5,7 @@ import Stdlib.Data.Nat open hiding {Ord; mkOrd};
 import Stdlib.Data.Nat.Ord as Ord;
 import Stdlib.Data.Pair as Ord;
 import Stdlib.Data.Bool.Base open;
-import Stdlib.Trait.Ord open using {Ordering; LT; EQ; GT; isLT; isGT};
+import Stdlib.Trait.Ord open using {Ordering; LessThan; Equal; GreaterThan; isLessThan; isGreaterThan};
 
 trait
 type Ord A :=
@@ -18,8 +18,8 @@ type Ord A :=
 mkOrdHelper
   {A}
   (cmp : A -> A -> Ordering)
-  {lt : A -> A -> Bool := λ {a b := isLT (cmp a b)}}
-  {gt : A -> A -> Bool := λ {a b := isGT (cmp a b)}}
+  {lt : A -> A -> Bool := λ {a b := isLessThan (cmp a b)}}
+  {gt : A -> A -> Bool := λ {a b := isGreaterThan (cmp a b)}}
   : Ord A := mkOrd cmp lt gt;
 
 ordNatNamed : Ord Nat :=
diff --git a/tests/Anoma/Compilation/positive/test071.juvix b/tests/Anoma/Compilation/positive/test071.juvix
index f5bd48deb0..e24bf1ec60 100644
--- a/tests/Anoma/Compilation/positive/test071.juvix
+++ b/tests/Anoma/Compilation/positive/test071.juvix
@@ -5,7 +5,7 @@ import Stdlib.Data.Nat open hiding {Ord; mkOrd};
 import Stdlib.Data.Nat.Ord as Ord;
 import Stdlib.Data.Pair as Ord;
 import Stdlib.Data.Bool.Base open;
-import Stdlib.Trait.Ord open using {Ordering; LT; EQ; GT; isLT; isGT};
+import Stdlib.Trait.Ord open using {Ordering; LessThan; Equal; GreaterThan; isLessThan; isGreaterThan};
 
 trait
 type Ord A :=
@@ -18,8 +18,8 @@ type Ord A :=
 mkOrdHelper
   {A}
   (cmp : A -> A -> Ordering)
-  {lt : A -> A -> Bool := λ {a b := isLT (cmp a b)}}
-  {gt : A -> A -> Bool := λ {a b := isGT (cmp a b)}}
+  {lt : A -> A -> Bool := λ {a b := isLessThan (cmp a b)}}
+  {gt : A -> A -> Bool := λ {a b := isGreaterThan (cmp a b)}}
   : Ord A :=
   mkOrd cmp lt gt;
 
diff --git a/tests/Casm/Compilation/positive/test069.juvix b/tests/Casm/Compilation/positive/test069.juvix
index ae81285b3c..3ed821fd77 100644
--- a/tests/Casm/Compilation/positive/test069.juvix
+++ b/tests/Casm/Compilation/positive/test069.juvix
@@ -5,7 +5,7 @@ import Stdlib.Data.Nat open hiding {Ord; mkOrd};
 import Stdlib.Data.Nat.Ord as Ord;
 import Stdlib.Data.Pair as Ord;
 import Stdlib.Data.Bool.Base open;
-import Stdlib.Trait.Ord open using {Ordering; LT; EQ; GT; isLT; isGT};
+import Stdlib.Trait.Ord open using {Ordering; LessThan; Equal; GreaterThan; isLessThan; isGreaterThan};
 
 trait
 type Ord A :=
@@ -18,8 +18,8 @@ type Ord A :=
 mkOrdHelper
   {A}
   (cmp : A -> A -> Ordering)
-  {lt : A -> A -> Bool := λ {a b := isLT (cmp a b)}}
-  {gt : A -> A -> Bool := λ {a b := isGT (cmp a b)}}
+  {lt : A -> A -> Bool := λ {a b := isLessThan (cmp a b)}}
+  {gt : A -> A -> Bool := λ {a b := isGreaterThan (cmp a b)}}
   : Ord A := mkOrd cmp lt gt;
 
 ordNatNamed : Ord Nat :=
diff --git a/tests/Casm/Compilation/positive/test071.juvix b/tests/Casm/Compilation/positive/test071.juvix
index f5bd48deb0..e24bf1ec60 100644
--- a/tests/Casm/Compilation/positive/test071.juvix
+++ b/tests/Casm/Compilation/positive/test071.juvix
@@ -5,7 +5,7 @@ import Stdlib.Data.Nat open hiding {Ord; mkOrd};
 import Stdlib.Data.Nat.Ord as Ord;
 import Stdlib.Data.Pair as Ord;
 import Stdlib.Data.Bool.Base open;
-import Stdlib.Trait.Ord open using {Ordering; LT; EQ; GT; isLT; isGT};
+import Stdlib.Trait.Ord open using {Ordering; LessThan; Equal; GreaterThan; isLessThan; isGreaterThan};
 
 trait
 type Ord A :=
@@ -18,8 +18,8 @@ type Ord A :=
 mkOrdHelper
   {A}
   (cmp : A -> A -> Ordering)
-  {lt : A -> A -> Bool := λ {a b := isLT (cmp a b)}}
-  {gt : A -> A -> Bool := λ {a b := isGT (cmp a b)}}
+  {lt : A -> A -> Bool := λ {a b := isLessThan (cmp a b)}}
+  {gt : A -> A -> Bool := λ {a b := isGreaterThan (cmp a b)}}
   : Ord A :=
   mkOrd cmp lt gt;
 
diff --git a/tests/Compilation/positive/test069.juvix b/tests/Compilation/positive/test069.juvix
index 98d49c65fe..3500b88af9 100644
--- a/tests/Compilation/positive/test069.juvix
+++ b/tests/Compilation/positive/test069.juvix
@@ -5,7 +5,7 @@ import Stdlib.Data.Nat open hiding {Ord; mkOrd};
 import Stdlib.Data.Nat.Ord as Ord;
 import Stdlib.Data.Pair as Ord;
 import Stdlib.Data.Bool.Base open;
-import Stdlib.Trait.Ord open using {Ordering; LT; EQ; GT; isLT; isGT};
+import Stdlib.Trait.Ord open using {Ordering; LessThan; Equal; GreaterThan; isLessThan; isGreaterThan};
 
 trait
 type Ord A :=
@@ -18,8 +18,8 @@ type Ord A :=
 mkOrdHelper
   {A}
   (cmp : A -> A -> Ordering)
-  {lt : A -> A -> Bool := λ {a b := isLT (cmp a b)}}
-  {gt : A -> A -> Bool := λ {a b := isGT (cmp a b)}}
+  {lt : A -> A -> Bool := λ {a b := isLessThan (cmp a b)}}
+  {gt : A -> A -> Bool := λ {a b := isGreaterThan (cmp a b)}}
   : Ord A := mkOrd cmp lt gt;
 
 ordNatNamed : Ord Nat :=
diff --git a/tests/Compilation/positive/test071.juvix b/tests/Compilation/positive/test071.juvix
index 3fce098625..0be40bf663 100644
--- a/tests/Compilation/positive/test071.juvix
+++ b/tests/Compilation/positive/test071.juvix
@@ -5,7 +5,7 @@ import Stdlib.Data.Nat open hiding {Ord; mkOrd};
 import Stdlib.Data.Nat.Ord as Ord;
 import Stdlib.Data.Pair as Ord;
 import Stdlib.Data.Bool.Base open;
-import Stdlib.Trait.Ord open using {Ordering; LT; EQ; GT; isLT; isGT};
+import Stdlib.Trait.Ord open using {Ordering; LessThan; Equal; GreaterThan; isLessThan; isGreaterThan};
 
 trait
 type Ord A :=
@@ -18,8 +18,8 @@ type Ord A :=
 mkOrdHelper
   {A}
   (cmp : A -> A -> Ordering)
-  {lt : A -> A -> Bool := λ {a b := isLT (cmp a b)}}
-  {gt : A -> A -> Bool := λ {a b := isGT (cmp a b)}}
+  {lt : A -> A -> Bool := λ {a b := isLessThan (cmp a b)}}
+  {gt : A -> A -> Bool := λ {a b := isGreaterThan (cmp a b)}}
   : Ord A := mkOrd cmp lt gt;
 
 instance
diff --git a/tests/Core/positive/test043.jvc b/tests/Core/positive/test043.jvc
index 7adfb28e3d..512087a7f8 100644
--- a/tests/Core/positive/test043.jvc
+++ b/tests/Core/positive/test043.jvc
@@ -2,32 +2,32 @@
 
 def fun :
    Π A : Type,
-   A → A :=
+   A -> A :=
    λ(A : Type)
    λ(x : A)
-   let f : (A → A) → A := λ(h : A → A) h (h x) in
+   let f : (A -> A) -> A := λ(h : A -> A) h (h x) in
    f (λ(y : A) x);
 
-def helper : Int → Int → Int :=
+def helper : Int -> Int -> Int :=
   λ(a : Int)
   λ(b : Int)
   a * b - b;
 
-def fun' : Π T : Type → Type,
+def fun' : Π T : Type -> Type,
            Π unused : Type,
            Π C : Type,
            Π A : Type,
-           (T A → A → C)
-           → A
-           → C :=
-  λ(T : Type → Type)
+           (T A -> A -> C)
+           -> A
+           -> C :=
+  λ(T : Type -> Type)
   λ(unused : Type)
   λ(C : Type)
   λ(A : Type)
-  λ(mhelper : T A → A → C)
+  λ(mhelper : T A -> A -> C)
   λ(a' : A)
-  let f : (A → A) → A := λ(g : A → A) g (g a') in
-  let h : A → A → C := λ(a1 : A) λ(a2 : A) mhelper a2 a1 in
+  let f : (A -> A) -> A := λ(g : A -> A) g (g a') in
+  let h : A -> A -> C := λ(a1 : A) λ(a2 : A) mhelper a2 a1 in
   f (λ(y : A) h y a');
 
 fun Int 2 + fun' (λ(A : Type) A) Bool Int Int helper 3
diff --git a/tests/Internal/positive/QuickSort.juvix b/tests/Internal/positive/QuickSort.juvix
index fb5c664302..f855a97223 100644
--- a/tests/Internal/positive/QuickSort.juvix
+++ b/tests/Internal/positive/QuickSort.juvix
@@ -13,7 +13,7 @@ quickSort
   | cmp (x :: xs) :=
     qsHelper
       x
-      (both (quickSort cmp) (partition (isGT << cmp x) xs));
+      (both (quickSort cmp) (partition (isGreaterThan << cmp x) xs));
 
 uniq
   : {A : Type} -> (A -> A -> Ordering) -> List A -> List A
@@ -21,7 +21,7 @@ uniq
   | _ y@(x :: nil) := y
   | cmp (x :: x' :: xs) :=
     ite
-      (isEQ (cmp x x'))
+      (isEqual (cmp x x'))
       (uniq cmp (x' :: xs))
       (x :: uniq cmp (x' :: xs));
 
diff --git a/tests/Internal/positive/out/FunctionType.out b/tests/Internal/positive/out/FunctionType.out
index 1e3bf3207c..644b032a97 100644
--- a/tests/Internal/positive/out/FunctionType.out
+++ b/tests/Internal/positive/out/FunctionType.out
@@ -1 +1 @@
-Π A : Type, Π B : Type, A → B
+Π A : Type, Π B : Type, A -> B
diff --git a/tests/Rust/Compilation/positive/test069.juvix b/tests/Rust/Compilation/positive/test069.juvix
index ae81285b3c..3ed821fd77 100644
--- a/tests/Rust/Compilation/positive/test069.juvix
+++ b/tests/Rust/Compilation/positive/test069.juvix
@@ -5,7 +5,7 @@ import Stdlib.Data.Nat open hiding {Ord; mkOrd};
 import Stdlib.Data.Nat.Ord as Ord;
 import Stdlib.Data.Pair as Ord;
 import Stdlib.Data.Bool.Base open;
-import Stdlib.Trait.Ord open using {Ordering; LT; EQ; GT; isLT; isGT};
+import Stdlib.Trait.Ord open using {Ordering; LessThan; Equal; GreaterThan; isLessThan; isGreaterThan};
 
 trait
 type Ord A :=
@@ -18,8 +18,8 @@ type Ord A :=
 mkOrdHelper
   {A}
   (cmp : A -> A -> Ordering)
-  {lt : A -> A -> Bool := λ {a b := isLT (cmp a b)}}
-  {gt : A -> A -> Bool := λ {a b := isGT (cmp a b)}}
+  {lt : A -> A -> Bool := λ {a b := isLessThan (cmp a b)}}
+  {gt : A -> A -> Bool := λ {a b := isGreaterThan (cmp a b)}}
   : Ord A := mkOrd cmp lt gt;
 
 ordNatNamed : Ord Nat :=
diff --git a/tests/Rust/Compilation/positive/test071.juvix b/tests/Rust/Compilation/positive/test071.juvix
index f5bd48deb0..e24bf1ec60 100644
--- a/tests/Rust/Compilation/positive/test071.juvix
+++ b/tests/Rust/Compilation/positive/test071.juvix
@@ -5,7 +5,7 @@ import Stdlib.Data.Nat open hiding {Ord; mkOrd};
 import Stdlib.Data.Nat.Ord as Ord;
 import Stdlib.Data.Pair as Ord;
 import Stdlib.Data.Bool.Base open;
-import Stdlib.Trait.Ord open using {Ordering; LT; EQ; GT; isLT; isGT};
+import Stdlib.Trait.Ord open using {Ordering; LessThan; Equal; GreaterThan; isLessThan; isGreaterThan};
 
 trait
 type Ord A :=
@@ -18,8 +18,8 @@ type Ord A :=
 mkOrdHelper
   {A}
   (cmp : A -> A -> Ordering)
-  {lt : A -> A -> Bool := λ {a b := isLT (cmp a b)}}
-  {gt : A -> A -> Bool := λ {a b := isGT (cmp a b)}}
+  {lt : A -> A -> Bool := λ {a b := isLessThan (cmp a b)}}
+  {gt : A -> A -> Bool := λ {a b := isGreaterThan (cmp a b)}}
   : Ord A :=
   mkOrd cmp lt gt;
 
diff --git a/tests/positive/265/M.juvix b/tests/positive/265/M.juvix
index 5f1dbc1a45..590437d7b4 100644
--- a/tests/positive/265/M.juvix
+++ b/tests/positive/265/M.juvix
@@ -4,8 +4,7 @@ type Bool :=
   | true : Bool
   | false : Bool;
 
-type Pair (A : Type) (B : Type) :=
-  mkPair : A → B → Pair A B;
+type Pair (A : Type) (B : Type) := mkPair : A → B → Pair A B;
 
 f : _ → _
   | (mkPair false true) := true
diff --git a/tests/positive/Internal/Positivity/RoseTree.juvix b/tests/positive/Internal/Positivity/RoseTree.juvix
index c8de6ff5ec..3b88717db1 100644
--- a/tests/positive/Internal/Positivity/RoseTree.juvix
+++ b/tests/positive/Internal/Positivity/RoseTree.juvix
@@ -4,5 +4,4 @@ type List (A : Type) : Type :=
   | nil : List A
   | cons : A -> List A -> List A;
 
-type RoseTree (A : Type) : Type :=
-  node : A -> List (RoseTree A) -> RoseTree A;
+type RoseTree (A : Type) : Type := node : A -> List (RoseTree A) -> RoseTree A;
diff --git a/tests/positive/Internal/Positivity2/main.juvix b/tests/positive/Internal/Positivity2/main.juvix
index d46d62baec..84f4f584f9 100644
--- a/tests/positive/Internal/Positivity2/main.juvix
+++ b/tests/positive/Internal/Positivity2/main.juvix
@@ -10,6 +10,7 @@ type Box (A : Type) := box A;
 
 module M1;
   type T1 (x y : Type) := mkT1 y (x -> x) x;
+
   type T2 (x : (Type -> Type) -> Type) := mkT2 (x (T1 T));
 end;
 
@@ -18,7 +19,7 @@ module M2;
 
   type T2 (x : Type) := mkT2 (x -> T);
 
-  -- type T3 := mkT3 (T1 T3);
+-- type T3 := mkT3 (T1 T3);
 end;
 
 module M3;
@@ -40,11 +41,11 @@ module E3;
 end;
 
 module E5;
-  type Ghost1 (A : Type) := ghost1 (Ghost2 ((Ghost1 (A -> A)) -> Ghost2 A));
+  type Ghost1 (A : Type) := ghost1 (Ghost2 (Ghost1 (A -> A) -> Ghost2 A));
 
   type Ghost2 (B : Type) := ghost2 Ok (Ghost1 B);
 
-  type Ok  := mkOk (Ghost1 (Ok -> Ok));
+  type Ok := mkOk (Ghost1 (Ok -> Ok));
 end;
 
 module E6;
diff --git a/tests/positive/Isabelle/Program.juvix b/tests/positive/Isabelle/Program.juvix
index 7e7db6324b..24d5ca0457 100644
--- a/tests/positive/Isabelle/Program.juvix
+++ b/tests/positive/Isabelle/Program.juvix
@@ -12,7 +12,7 @@ id2 {A : Type} : A -> A := id;
 add_one : List Nat -> List Nat
   | [] := []
   -- hello!
-  | (x :: xs) := (x + 1) :: add_one xs;
+  | (x :: xs) := x + 1 :: add_one xs;
 
 sum : List Nat -> Nat
   | [] := 0
@@ -37,14 +37,20 @@ dec : Nat -> Nat
 dec' (x : Nat) : Nat :=
   -- Do case switch
   -- pattern match on x
-  case x of {- the zero case -} zero := {- return zero -} zero | {- the suc case -} suc y := y;
+  case x of
+    | {- the zero case -}
+    zero :=
+      {- return zero -}
+      zero
+    | {- the suc case -}
+    suc y := y;
 
 optmap {A} (f : A -> A) : Maybe A -> Maybe A
   | nothing := nothing
   | (just x) := just (f x);
 
 pboth {A B A' B'} (f : A -> A') (g : B -> B') : Pair A B -> Pair A' B'
-  | (x, y) := (f x, g y);
+  | (x, y) := f x, g y;
 
 bool_fun (x y z : Bool) : Bool := x && y || z;
 
@@ -62,26 +68,26 @@ qsnd : {A : Type} → Queue A → List A
   | (queue _ v) := v;
 
 pop_front {A} (q : Queue A) : Queue A :=
-    let
-      q' : Queue A := queue (tail (qfst q)) (qsnd q);
-    in case qfst q' of
-         | nil := queue (reverse (qsnd q')) nil
-         | _ := q';
+  let
+    q' : Queue A := queue (tail (qfst q)) (qsnd q);
+  in case qfst q' of
+       | nil := queue (reverse (qsnd q')) nil
+       | _ := q';
 
 push_back {A} (q : Queue A) (x : A) : Queue A :=
-    case qfst q of
-      | nil := queue (x :: nil) (qsnd q)
-      | q' := queue q' (x :: qsnd q);
+  case qfst q of
+    | nil := queue (x :: nil) (qsnd q)
+    | q' := queue q' (x :: qsnd q);
 
 --- Checks if the queue is empty
 is_empty {A} (q : Queue A) : Bool :=
-    case qfst q of
-      | nil :=
-        case qsnd q of {
-          | nil := true
-          | _ := false
-        }
-      | _ := false;
+  case qfst q of
+    | nil :=
+      case qsnd q of {
+        | nil := true
+        | _ := false
+      }
+    | _ := false;
 
 empty : {A : Type} → Queue A := queue nil nil;
 
@@ -96,52 +102,85 @@ funkcja (n : Nat) : Nat :=
 
 --- An Either' type
 type Either' A B :=
-  --- Left constructor
-  Left' A
-| --- Right constructor
-  Right' B;
+  | --- Left constructor
+    Left' A
+  | --- Right constructor
+    Right' B;
 
 -- Records
 
 {-# isabelle-ignore: true #-}
-type R' := mkR' {
-  r1' : Nat;
-  r2' : Nat;
-};
-
-type R := mkR {
-  r1 : Nat;
-  r2 : Nat;
-};
+type R' :=
+  mkR' {
+    r1' : Nat;
+    r2' : Nat
+  };
+
+type R :=
+  mkR {
+    r1 : Nat;
+    r2 : Nat
+  };
 
 r : R := mkR 0 1;
+
 v : Nat := 0;
 
-funR (r : R) : R :=
-  case r of
-  | mkR@{r1; r2} := r@R{r1 := r1 + r2};
+funR (r : R) : R := case r of mkR@{r1; r2} := r@R{r1 := r1 + r2};
 
 funRR : R -> R
   | r@mkR@{r1; r2} := r@R{r1 := r1 + r2};
 
 funR' : R -> R
-  | mkR@{r1 := rr1; r2 := rr2} := mkR@{r1 := rr1 + rr2; r2 := rr2};
+  | mkR@{r1 := rr1; r2 := rr2} :=
+    mkR@{
+      r1 := rr1 + rr2;
+      r2 := rr2
+    };
 
 funR1 : R -> R
-  | mkR@{r1 := zero; r2} := mkR@{r1 := r2; r2}
-  | mkR@{r1 := rr1; r2 := rr2} := mkR@{r1 := rr2; r2 := rr1};
+  | mkR@{r1 := zero; r2} :=
+    mkR@{
+      r1 := r2;
+      r2
+    }
+  | mkR@{r1 := rr1; r2 := rr2} :=
+    mkR@{
+      r1 := rr2;
+      r2 := rr1
+    };
 
 funR2 (r : R) : R :=
   case r of
-  | mkR@{r1 := zero; r2} := mkR@{r1 := r2; r2}
-  | mkR@{r1 := rr1; r2 := rr2} := mkR@{r1 := rr2; r2 := rr1};
+    | mkR@{r1 := zero; r2} :=
+      mkR@{
+        r1 := r2;
+        r2
+      }
+    | mkR@{r1 := rr1; r2 := rr2} :=
+      mkR@{
+        r1 := rr2;
+        r2 := rr1
+      };
 
 funR3 (er : Either' R R) : R :=
   case er of
-  | Left' mkR@{r1 := zero; r2} := mkR@{r1 := r2; r2}
-  | Left' mkR@{r1 := rr1; r2 := rr2} := mkR@{r1 := rr2; r2 := rr1}
-  | Right' mkR@{r1; r2 := zero} := mkR@{r1 := 7; r2 := r1}
-  | Right' r@(mkR@{r1; r2}) := r@R{r1 := r2 + 2; r2 := r1 + 3};
+    | Left' mkR@{r1 := zero; r2} :=
+      mkR@{
+        r1 := r2;
+        r2
+      }
+    | Left' mkR@{r1 := rr1; r2 := rr2} :=
+      mkR@{
+        r1 := rr2;
+        r2 := rr1
+      }
+    | Right' mkR@{r1; r2 := zero} :=
+      mkR@{
+        r1 := 7;
+        r2 := r1
+      }
+    | Right' r@mkR@{r1; r2} := r@R{   r1 := r2 + 2; r2 := r1 + 3 };
 
 funR4 : R -> R
   | r@mkR@{r1} := r@R{r2 := r1};
diff --git a/tests/positive/MarkdownImport/B.juvix.md b/tests/positive/MarkdownImport/B.juvix.md
index 6d596fc858..02b723a94d 100644
--- a/tests/positive/MarkdownImport/B.juvix.md
+++ b/tests/positive/MarkdownImport/B.juvix.md
@@ -1,5 +1,5 @@
 ```juvix
 module B;
 
-axiom D : Type; 
-```
\ No newline at end of file
+axiom D : Type;
+```
diff --git a/tests/positive/MarkdownImport/C.juvix.md b/tests/positive/MarkdownImport/C.juvix.md
index 2d8d4f0b09..90be1e4501 100644
--- a/tests/positive/MarkdownImport/C.juvix.md
+++ b/tests/positive/MarkdownImport/C.juvix.md
@@ -12,4 +12,4 @@ Text in between code blocks
 
 ```juvix
 axiom b : D;
-```
\ No newline at end of file
+```
diff --git a/tests/positive/Termination/Data/List.juvix b/tests/positive/Termination/Data/List.juvix
index 2d9e8f1a66..2bde073fe8 100644
--- a/tests/positive/Termination/Data/List.juvix
+++ b/tests/positive/Termination/Data/List.juvix
@@ -11,13 +11,11 @@ type List (A : Type) :=
   | cons : A → List A → List A;
 
 -- Do not remove implicit arguments. Useful for testing.
-foldr
-  : {A : Type} → {B : Type} → (A → B → B) → B → List A → B
+foldr : {A : Type} → {B : Type} → (A → B → B) → B → List A → B
   | _ z nil := z
   | f z (cons h hs) := f h (foldr {_} f z hs);
 
-foldl
-  : {A : Type} → {B : Type} → (B → A → B) → B → List A → B
+foldl : {A : Type} → {B : Type} → (B → A → B) → B → List A → B
   | f z nil := z
   | {_} {_} f z (cons h hs) := foldl {_} f (f z h) hs;
 
@@ -27,8 +25,7 @@ map : {A : Type} → {B : Type} → (A → B) → List A → List B
 
 filter : {A : Type} → (A → Bool) → List A → List A
   | f nil := nil
-  | f (cons h hs) :=
-    ite (f h) (cons h (filter {_} f hs)) (filter f hs);
+  | f (cons h hs) := ite (f h) (cons h (filter {_} f hs)) (filter f hs);
 
 length : {A : Type} → List A → ℕ
   | nil := zero
diff --git a/tests/positive/issue1693/M.juvix b/tests/positive/issue1693/M.juvix
index 68bb4ffd77..10b95c16c1 100644
--- a/tests/positive/issue1693/M.juvix
+++ b/tests/positive/issue1693/M.juvix
@@ -2,14 +2,7 @@ module M;
 
 import Stdlib.Prelude open;
 
-S
-  : {A : Type}
-    → {B : Type}
-    → {C : Type}
-    → (A → B → C)
-    → (A → B)
-    → A
-    → C
+S : {A : Type} → {B : Type} → {C : Type} → (A → B → C) → (A → B) → A → C
   | x y z := x z (y z);
 
 K : {A : Type} → {B : Type} → A → B → A
diff --git a/tests/positive/issue1731/builtinFail.juvix b/tests/positive/issue1731/builtinFail.juvix
index a665df7900..4ea27d9e1f 100644
--- a/tests/positive/issue1731/builtinFail.juvix
+++ b/tests/positive/issue1731/builtinFail.juvix
@@ -6,7 +6,4 @@ import Stdlib.System.IO open;
 builtin fail
 axiom fail : {A : Type} → String → A;
 
-main : IO :=
-  printStringLn "Get"
-    >>> fail "Enough"
-    >>> printStringLn "Sleep";
+main : IO := printStringLn "Get" >>> fail "Enough" >>> printStringLn "Sleep";
diff --git a/tests/positive/issue3048/Other.juvix b/tests/positive/issue3048/Other.juvix
index e947739e98..d4d31a8fb5 100644
--- a/tests/positive/issue3048/Other.juvix
+++ b/tests/positive/issue3048/Other.juvix
@@ -1,5 +1,7 @@
 module Other;
 
 type T1 := mkT1;
+
 type T2 := mkT2;
+
 type T3 := mkT3;
diff --git a/tests/positive/issue3048/Package.juvix b/tests/positive/issue3048/Package.juvix
index 6e4702c194..f04d2d888f 100644
--- a/tests/positive/issue3048/Package.juvix
+++ b/tests/positive/issue3048/Package.juvix
@@ -4,7 +4,5 @@ import PackageDescription.V2 open;
 
 package : Package :=
   defaultPackage@?{
-    name := "issue3048";
-    dependencies :=
-      [github "anoma" "juvix-stdlib" "v0.7.0"; github "anoma" "juvix-containers" "v0.15.0"]
+    name := "issue3048"
   };
diff --git a/tests/positive/issue3048/main.juvix b/tests/positive/issue3048/main.juvix
index 4681b7ecb9..12fe495c39 100644
--- a/tests/positive/issue3048/main.juvix
+++ b/tests/positive/issue3048/main.juvix
@@ -2,15 +2,7 @@ module main;
 
 import Other;
 
-type AVLTree (A : Type) :=
-  node (AVLTree A)
-       (AVLTree A)
-       (AVLTree A)
-       (AVLTree A)
-       (AVLTree A)
-       (AVLTree A)
-       (AVLTree A)
-       (AVLTree A)
-       (AVLTree A);
+type Tree (A : Type) :=
+  node (Tree A) (Tree A) (Tree A) (Tree A) (Tree A) (Tree A) (Tree A) (Tree A) (Tree A);
 
-type Foo := mkFoo (AVLTree Foo);
+type Foo := mkFoo (Tree Foo);
diff --git a/tests/smoke/Commands/dev/repl.smoke.yaml b/tests/smoke/Commands/dev/repl.smoke.yaml
index da65c96176..e22e0a6a96 100644
--- a/tests/smoke/Commands/dev/repl.smoke.yaml
+++ b/tests/smoke/Commands/dev/repl.smoke.yaml
@@ -74,7 +74,7 @@ tests:
       - dev
       - repl
     stdout:
-      contains: "{A : Type} → List A → Bool"
+      contains: "{A : Type} -> List A -> Bool"
     stdin: ":type null"
     exit-status: 0
 
@@ -84,7 +84,7 @@ tests:
       - dev
       - repl
     stdout:
-      contains: "Nat → Nat"
+      contains: "Nat -> Nat"
     stdin: ":type suc"
     exit-status: 0
 
@@ -94,7 +94,7 @@ tests:
       - dev
       - repl
     stdout:
-      contains: "Nat → Nat"
+      contains: "Nat -> Nat"
     stdin: ":t suc"
     exit-status: 0
 
@@ -105,7 +105,7 @@ tests:
       script: |
         cd ./../juvix-stdlib && juvix repl Stdlib/Prelude.juvix
     stdout:
-      contains: "Nat → Nat"
+      contains: "Nat -> Nat"
     stdin: ":t suc"
     exit-status: 0
 
diff --git a/tests/smoke/Commands/repl.smoke.yaml b/tests/smoke/Commands/repl.smoke.yaml
index cb930c5f2b..bd50a8d8fb 100644
--- a/tests/smoke/Commands/repl.smoke.yaml
+++ b/tests/smoke/Commands/repl.smoke.yaml
@@ -75,7 +75,7 @@ tests:
     stdout:
       contains: |
         builtin IO-sequence
-        axiom >>> : IO → IO → IO
+        axiom >>> : IO -> IO -> IO
     exit-status: 0
 
   - name: repl-def-infix
@@ -87,7 +87,7 @@ tests:
     stdout:
       contains: |
         builtin IO-sequence
-        axiom >>> : IO → IO → IO
+        axiom >>> : IO -> IO -> IO
     exit-status: 0
 
   - name: open
@@ -156,7 +156,7 @@ tests:
       - juvix
       - repl
     stdout:
-      contains: "{A : Type} → List A → Bool"
+      contains: "{A : Type} -> (list : List A) -> Bool"
     stdin: ":type null"
     exit-status: 0
 
@@ -165,7 +165,7 @@ tests:
       - juvix
       - repl
     stdout:
-      contains: "Nat → Nat"
+      contains: "Nat -> Nat"
     stdin: ":type suc"
     exit-status: 0
 
@@ -174,7 +174,7 @@ tests:
       - juvix
       - repl
     stdout:
-      contains: "Nat → Nat"
+      contains: "Nat -> Nat"
     stdin: ":t suc"
     exit-status: 0
 
@@ -185,7 +185,7 @@ tests:
       script: |
         cd ./../juvix-stdlib && juvix repl Stdlib/Prelude.juvix
     stdout:
-      contains: "Nat → Nat"
+      contains: "Nat -> Nat"
     stdin: ":t suc"
     exit-status: 0
 
@@ -353,7 +353,7 @@ tests:
     stdin: ":t (\\(A : Type) \\(x : A) \\(y : A) \\(B : Type) \\(z : B) \\(_ : A) x) Int 1 2 String"
     stdout:
       contains: |
-        String → Int → Int
+        String -> Int -> Int
 
   - name: repl-import-no-dependencies
     command: