diff --git a/examples/milestone/Collatz/Collatz.juvix b/examples/milestone/Collatz/Collatz.juvix
index da8db0a8ed..810611c350 100644
--- a/examples/milestone/Collatz/Collatz.juvix
+++ b/examples/milestone/Collatz/Collatz.juvix
@@ -6,15 +6,15 @@ mapMaybe : {A : Type} → {B : Type} → (A → B) → Maybe A → Maybe B;
 mapMaybe _ nothing := nothing;
 mapMaybe f (just x) := just (f x);
 
-div2 : ℕ → Maybe ℕ;
+div2 : Nat → Maybe Nat;
 div2 zero := just zero;
 div2 (suc (suc n)) := mapMaybe suc (div2 n);
 div2 _ := nothing;
 
-collatzNext : ℕ → ℕ;
+collatzNext : Nat → Nat;
 collatzNext n := fromMaybe (suc (3 * n)) (div2 n);
 
-collatz : ℕ → ℕ;
+collatz : Nat → Nat;
 collatz zero := zero;
 collatz (suc zero) := suc zero;
 collatz (suc (suc n)) := collatzNext (suc (suc n));
@@ -28,20 +28,20 @@ compile readline {
   c ↦ "readline()";
 };
 
-axiom parsePositiveInt : String → ℕ;
+axiom parsePositiveInt : String → Nat;
 
 compile parsePositiveInt {
   c ↦ "parsePositiveInt";
 };
 
-getInitial : ℕ;
+getInitial : Nat;
 getInitial := parsePositiveInt (readline);
 
-output : ℕ → ℕ × IO;
+output : Nat → Nat × IO;
 output n := (n, putStrLn (natToStr n));
 
 terminating
-run : (ℕ → ℕ) → ℕ → IO;
+run : (Nat → Nat) → Nat → IO;
 run _ (suc zero) := putStrLn "Finished!";
 run f n := run f (fst (output (f n)));
 
diff --git a/examples/milestone/Fibonacci/Fibonacci.juvix b/examples/milestone/Fibonacci/Fibonacci.juvix
index a8c3755fbf..5cc8025e54 100644
--- a/examples/milestone/Fibonacci/Fibonacci.juvix
+++ b/examples/milestone/Fibonacci/Fibonacci.juvix
@@ -2,11 +2,11 @@ module Fibonacci;
 
 open import Stdlib.Prelude;
 
-fib : ℕ → ℕ → ℕ → ℕ;
+fib : Nat → Nat → Nat → Nat;
 fib zero x1 _ := x1;
 fib (suc n) x1 x2 := fib n x2 (x1 + x2);
 
-fibonacci : ℕ → ℕ;
+fibonacci : Nat → Nat;
 fibonacci n := fib n 0 1;
 
 main : IO;
diff --git a/examples/milestone/Hanoi/Hanoi.juvix b/examples/milestone/Hanoi/Hanoi.juvix
index c5437042c3..93de2ada39 100644
--- a/examples/milestone/Hanoi/Hanoi.juvix
+++ b/examples/milestone/Hanoi/Hanoi.juvix
@@ -38,8 +38,8 @@ unlines := intercalate "\n";
 singleton : {A : Type} → A → List A;
 singleton a := a ∷ nil;
 
---- Produce a ;String; representation of a ;List ℕ;
-showList : List ℕ → String;
+--- Produce a ;String; representation of a ;List Nat;
+showList : List Nat → String;
 showList xs := "[" ++str intercalate "," (map natToStr xs) ++str "]";
 
 --- A Peg represents a peg in the towers of Hanoi game
@@ -64,7 +64,7 @@ showMove : Move → String;
 showMove (move from to) := showPeg from ++str " -> " ++str showPeg to;
 
 --- Produce a list of ;Move;s that solves the towers of Hanoi game
-hanoi : ℕ → Peg → Peg → Peg → List Move;
+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;
 
diff --git a/examples/milestone/PascalsTriangle/PascalsTriangle.juvix b/examples/milestone/PascalsTriangle/PascalsTriangle.juvix
index cd33f66903..7d65af56b3 100644
--- a/examples/milestone/PascalsTriangle/PascalsTriangle.juvix
+++ b/examples/milestone/PascalsTriangle/PascalsTriangle.juvix
@@ -15,7 +15,7 @@ zipWith f _ nil := nil;
 zipWith f (x ∷ xs) (y ∷ ys) := f x y ∷ zipWith f xs ys;
 
 --- Return a list of repeated applications of a given function
-iterate : {A : Type} → ℕ → (A → A) → A → List A;
+iterate : {A : Type} → Nat → (A → A) → A → List A;
 iterate zero _ _ := nil;
 iterate (suc n) f a := a ∷ iterate n f (f a);
 
@@ -43,15 +43,15 @@ intercalate sep xs := concat (intersperse sep xs);
 unlines : List String → String;
 unlines := intercalate "\n";
 
-showList : List ℕ → String;
+showList : List Nat → String;
 showList xs := "[" ++str intercalate "," (map natToStr xs) ++str "]";
 
 --- Compute the next row of Pascal's triangle
-pascalNextRow : List ℕ → List ℕ;
+pascalNextRow : List Nat → List Nat;
 pascalNextRow row := zipWith (+) (singleton zero ++ row) (row ++ singleton zero);
 
 --- Produce Pascal's triangle to a given depth
-pascal : ℕ → List (List ℕ);
+pascal : Nat → List (List Nat);
 pascal rows := iterate rows pascalNextRow (singleton one);
 
 main : IO;
diff --git a/examples/milestone/TicTacToe/CLI/TicTacToe.juvix b/examples/milestone/TicTacToe/CLI/TicTacToe.juvix
index 60cacf1bc2..440c532cb3 100644
--- a/examples/milestone/TicTacToe/CLI/TicTacToe.juvix
+++ b/examples/milestone/TicTacToe/CLI/TicTacToe.juvix
@@ -16,14 +16,14 @@ compile readline {
   c ↦ "readline()";
 };
 
-axiom parsePositiveInt : String → ℕ;
+axiom parsePositiveInt : String → Nat;
 
 compile parsePositiveInt {
   c ↦ "parsePositiveInt";
 };
 
--- | Reads a ;ℕ; from stdin
-getMove : Maybe ℕ;
+-- | Reads a ;Nat; from stdin
+getMove : Maybe Nat;
 getMove := validMove (parsePositiveInt (readline));
 
 do : IO × GameState -> GameState;
diff --git a/examples/milestone/TicTacToe/Logic/Board.juvix b/examples/milestone/TicTacToe/Logic/Board.juvix
index 903318ed25..c5a297a756 100644
--- a/examples/milestone/TicTacToe/Logic/Board.juvix
+++ b/examples/milestone/TicTacToe/Logic/Board.juvix
@@ -11,7 +11,7 @@ inductive Board {
 };
 
 --- Returns the list of numbers corresponding to the empty ;Square;s
-possibleMoves : List Square → List ℕ;
+possibleMoves : List Square → List Nat;
 possibleMoves nil := nil;
 possibleMoves ((empty n) ∷ xs) := n ∷ possibleMoves xs;
 possibleMoves (_ ∷ xs) := possibleMoves xs;
diff --git a/examples/milestone/TicTacToe/Logic/Game.juvix b/examples/milestone/TicTacToe/Logic/Game.juvix
index 89894892a6..45351b0b32 100644
--- a/examples/milestone/TicTacToe/Logic/Game.juvix
+++ b/examples/milestone/TicTacToe/Logic/Game.juvix
@@ -22,7 +22,7 @@ checkState (state b p e) :=
          (state b p e));
 
 --- Given a player attempted move, updates the state accordingly.
-playMove : Maybe ℕ → GameState → GameState;
+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) :=
@@ -32,8 +32,8 @@ playMove (just k) (state (board s) player e) :=
                            (switch player)
                            noError));
 
---- Returns ;just; if the given ;ℕ; is in range of 1..9
-validMove : ℕ → Maybe ℕ;
+--- Returns ;just; if the given ;Nat; is in range of 1..9
+validMove : Nat → Maybe Nat;
 validMove n := if ((n <= nine) && (n >= one)) (just n) nothing;
 
 end;
diff --git a/examples/milestone/TicTacToe/Logic/Square.juvix b/examples/milestone/TicTacToe/Logic/Square.juvix
index 55b5229acb..f1953dd981 100644
--- a/examples/milestone/TicTacToe/Logic/Square.juvix
+++ b/examples/milestone/TicTacToe/Logic/Square.juvix
@@ -7,8 +7,8 @@ open import Logic.Extra;
 
 --- A square is each of the holes in a board
 inductive Square {
-  --- An empty square has a ;ℕ; that uniquely identifies it
-  empty : ℕ → Square;
+  --- An empty square has a ;Nat; that uniquely identifies it
+  empty : Nat → Square;
   --- An occupied square has a ;Symbol; in it
   occupied : Symbol → Square;
 };
@@ -24,7 +24,7 @@ showSquare : Square → String;
 showSquare (empty n) := " " ++str natToStr n ++str " ";
 showSquare (occupied s) := " " ++str showSymbol s ++str " ";
 
-replace : Symbol → ℕ → Square → Square;
+replace : Symbol → Nat → Square → Square;
 replace player k (empty n) := if (n Stdlib.Data.Nat.Ord.== k) (occupied player) (empty n);
 replace _ _ s := s;
 
diff --git a/examples/milestone/TicTacToe/Web/TicTacToe.juvix b/examples/milestone/TicTacToe/Web/TicTacToe.juvix
index a3b010e0e9..80efc21bea 100644
--- a/examples/milestone/TicTacToe/Web/TicTacToe.juvix
+++ b/examples/milestone/TicTacToe/Web/TicTacToe.juvix
@@ -16,10 +16,10 @@ open import Logic.Game;
 axiom hostLog : String → IO;
 
 -- XCoord → YCoord → Width → Height → Color → IO
-axiom hostFillRect : ℕ → ℕ → ℕ → ℕ → String → IO;
+axiom hostFillRect : Nat → Nat → Nat → Nat → String → IO;
 
 -- XCoord → YCoord → Text → Size → Color → Align → IO
-axiom hostFillText : ℕ → ℕ → String → ℕ → String → ℕ → IO;
+axiom hostFillText : Nat → Nat → String → Nat → String → Nat → IO;
 
 -- Nat extension
 
@@ -30,7 +30,7 @@ foreign c {
 };
 
 infixl 7 div;
-axiom div : ℕ → ℕ → ℕ;
+axiom div : Nat → Nat → Nat;
 
 compile div {
   c ↦ "div";
@@ -55,31 +55,31 @@ zip : {A : Type} → {B : Type} → List A → List B → List (A × B);
 zip (a ∷ as) (b ∷ bs) := (a, b) ∷ zip as bs;
 zip _ _ := nil;
 
-rangeAux : ℕ → ℕ → List ℕ;
+rangeAux : Nat → Nat → List Nat;
 rangeAux _ zero := nil;
 rangeAux m (suc n) := m ∷ rangeAux (suc m) n;
 
-range : ℕ → List ℕ;
+range : Nat → List Nat;
 range n := rangeAux zero n;
 
-enumerate : {A : Type} → List A → List (ℕ × A);
+enumerate : {A : Type} → List A → List (Nat × A);
 enumerate l := zip (range (length l)) l;
 
 -- Formatting constants
 
-squareWidth : ℕ;
+squareWidth : Nat;
 squareWidth := 100;
 
-textSize : ℕ;
+textSize : Nat;
 textSize := 30;
 
-xTextOffset : ℕ;
+xTextOffset : Nat;
 xTextOffset := 50;
 
-yTextOffset : ℕ;
+yTextOffset : Nat;
 yTextOffset := 60;
 
-canvasPadding : ℕ;
+canvasPadding : Nat;
 canvasPadding := 8;
 
 textColor : String;
@@ -99,21 +99,21 @@ inductive Align {
   center : Align;
 };
 
-alignNum : Align → ℕ;
+alignNum : Align → Nat;
 alignNum left := zero;
 alignNum right := one;
 alignNum center := two;
 
-renderText : String → ℕ → ℕ → Align → IO;
+renderText : String → Nat → Nat → Align → IO;
 renderText t row col a := hostFillText ((squareWidth * row) + xTextOffset) ((squareWidth * col) + yTextOffset) t textSize textColor (alignNum a);
 
-renderSymbol : Symbol → ℕ → ℕ → IO;
+renderSymbol : Symbol → Nat → Nat → IO;
 renderSymbol s row col := renderText (showSymbol s) row col center;
 
-renderNumber : ℕ → ℕ → ℕ → IO;
+renderNumber : Nat → Nat → Nat → IO;
 renderNumber n row col := renderText (natToStr n) row col center;
 
-renderSquare : ℕ → ℕ → Square → IO;
+renderSquare : Nat → Nat → Square → IO;
 renderSquare row col (occupied s) :=
     hostFillRect (squareWidth * row) (squareWidth * col) squareWidth squareWidth backgroundColor
     >> renderSymbol s row col;
@@ -121,10 +121,10 @@ renderSquare row col (empty n) :=
     hostFillRect (squareWidth * row) (squareWidth * col) squareWidth squareWidth lightBackgroundColor
     >> renderNumber n row col;
 
-renderRowAux : ℕ → (ℕ × Square) → IO;
+renderRowAux : Nat → (Nat × Square) → IO;
 renderRowAux col (row, s) := renderSquare row col s;
 
-renderRow : ℕ × (List Square) → IO;
+renderRow : Nat × (List Square) → IO;
 renderRow (n, xs) := mapIO (renderRowAux n) (enumerate xs);
 
 renderBoard : Board → IO;
@@ -149,7 +149,7 @@ renderGameState (state b p _) := renderBoard b >> renderFooterText (nextPlayerTe
 renderAndReturn : GameState → GameState;
 renderAndReturn s := const s (renderGameState s);
 
-selectedSquare : ℕ → ℕ → ℕ;
+selectedSquare : Nat → Nat → Nat;
 selectedSquare row col := 3 * (col div squareWidth) + (row div squareWidth) + 1;
 
 -- API
@@ -157,7 +157,7 @@ selectedSquare row col := 3 * (col div squareWidth) + (row div squareWidth) + 1;
 initGame : GameState;
 initGame := const beginState (renderGameState beginState >> renderText "Click on a square to make a move" 0 4 left);
 
-move : GameState → ℕ → ℕ → GameState;
+move : GameState → Nat → Nat → GameState;
 move (state b p (terminate e)) x y := renderAndReturn (state b p (terminate e));
 move s x y := renderAndReturn (playMove (validMove (selectedSquare x y)) s);
 
diff --git a/tests/positive/Internal/LiteralInt.juvix b/tests/positive/Internal/LiteralInt.juvix
index 949ff2b81b..0ccc415c3e 100644
--- a/tests/positive/Internal/LiteralInt.juvix
+++ b/tests/positive/Internal/LiteralInt.juvix
@@ -8,6 +8,6 @@ module LiteralInt;
     b : B;
   };
 
-  f : ℕ;
+  f : Nat;
   f := 1;
 end;
diff --git a/tests/positive/MiniC/ExportName/Input.juvix b/tests/positive/MiniC/ExportName/Input.juvix
index 74d42799d5..f6a2c96bca 100644
--- a/tests/positive/MiniC/ExportName/Input.juvix
+++ b/tests/positive/MiniC/ExportName/Input.juvix
@@ -2,7 +2,7 @@ module Input;
 
 open import Stdlib.Prelude;
 
-fun : ℕ;
+fun : Nat;
 fun := six;
 
 end;
diff --git a/tests/positive/MiniC/ExportNameArgs/Input.juvix b/tests/positive/MiniC/ExportNameArgs/Input.juvix
index e06702b538..d3e4fdc90c 100644
--- a/tests/positive/MiniC/ExportNameArgs/Input.juvix
+++ b/tests/positive/MiniC/ExportNameArgs/Input.juvix
@@ -2,7 +2,7 @@ module Input;
 
 open import Stdlib.Prelude;
 
-fun : ℕ → ℕ;
+fun : Nat → Nat;
 fun _ := three;
 
 end;
diff --git a/tests/positive/StdlibImport/StdlibImport.juvix b/tests/positive/StdlibImport/StdlibImport.juvix
index 6641da1142..b88a78860d 100644
--- a/tests/positive/StdlibImport/StdlibImport.juvix
+++ b/tests/positive/StdlibImport/StdlibImport.juvix
@@ -4,7 +4,7 @@ open import Stdlib.Prelude;
 
 import A;
 
-two : ℕ;
+two : Nat;
 two := 1 + 1;
 
 foo : A.Foo;
diff --git a/tests/positive/Symbols.juvix b/tests/positive/Symbols.juvix
index 136ff61458..9449085c28 100644
--- a/tests/positive/Symbols.juvix
+++ b/tests/positive/Symbols.juvix
@@ -2,30 +2,30 @@ module Symbols;
 
   open import Stdlib.Data.Nat;
 
-  ╘⑽╛ : ℕ;
+  ╘⑽╛ : Nat;
   ╘⑽╛ := suc nine;
 
    -- no - function!?
-   - : ℕ -> ℕ -> ℕ;
+   - : Nat -> Nat -> Nat;
    - := (+);
 
-  （-） : ℕ -> ℕ -> ℕ;
+  （-） : Nat -> Nat -> Nat;
   （-） := (-);
 
-  （*） : ℕ -> ℕ -> ℕ;
+  （*） : Nat -> Nat -> Nat;
   （*） := (*);
 
   infixl 6 －;
-  － : ℕ -> ℕ -> ℕ;
+  － : Nat -> Nat -> Nat;
   － := （-）;
 
   infixl 7 ·;
-  · : ℕ -> ℕ -> ℕ;
+  · : Nat -> Nat -> Nat;
   · := （*）;
 
-  （0） : ℕ;
+  （0） : Nat;
   （0） := ╘⑽╛ － ╘⑽╛ · zero;
 
-  主功能 : ℕ;
+  主功能 : Nat;
   主功能 := （0）;
-end;
\ No newline at end of file
+end;