diff --git a/examples/demo/Demo.juvix b/examples/demo/Demo.juvix
index 1f58f2a5d7..30c07d1672 100644
--- a/examples/demo/Demo.juvix
+++ b/examples/demo/Demo.juvix
@@ -2,9 +2,6 @@ module Demo;
 
 -- standard library prelude
 import Stdlib.Prelude open;
--- for comparisons on natural numbers
-import Stdlib.Data.Nat.Ord open;
--- for Ordering
 
 even : Nat → Bool
   | zero := true
@@ -35,13 +32,13 @@ preorder : {A : Type} → Tree A → List A
   | (node x l r) := x :: nil ++ preorder l ++ preorder r;
 
 terminating
-sort : {A : Type} → (A → A → Ordering) → List A → List A
-  | _ nil := nil
-  | _ xs@(_ :: nil) := xs
-  | {A} cmp xs :=
+sort {A} {{Ord A}} : List A → List A
+  | nil := nil
+  | xs@(_ :: nil) := xs
+  | xs :=
     uncurry
-      (merge {{mkOrd cmp}})
-      (both (sort cmp) (splitAt (div (length xs) 2) xs));
+      merge
+      (both sort (splitAt (div (length xs) 2) xs));
 
 printNatListLn : List Nat → IO
   | nil := printStringLn "nil"
@@ -51,6 +48,6 @@ printNatListLn : List Nat → IO
 main : IO :=
   printStringLn "Hello!"
     >> printNatListLn (preorder (mirror tree))
-    >> printNatListLn (sort compare (preorder (mirror tree)))
+    >> printNatListLn (sort (preorder (mirror tree)))
     >> printNatLn (log2 3)
     >> printNatLn (log2 130);
diff --git a/examples/midsquare/MidSquareHash.juvix b/examples/midsquare/MidSquareHash.juvix
index 175d2bc949..cafd295dbe 100644
--- a/examples/midsquare/MidSquareHash.juvix
+++ b/examples/midsquare/MidSquareHash.juvix
@@ -5,7 +5,6 @@
 module MidSquareHash;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 --- `pow N` is 2 ^ N
 pow : Nat -> Nat
diff --git a/examples/midsquare/MidSquareHashUnrolled.juvix b/examples/midsquare/MidSquareHashUnrolled.juvix
index 602d0c330c..d9f0710300 100644
--- a/examples/midsquare/MidSquareHashUnrolled.juvix
+++ b/examples/midsquare/MidSquareHashUnrolled.juvix
@@ -6,7 +6,6 @@
 module MidSquareHashUnrolled;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 --- `powN` is 2 ^ N
 pow0 : Nat := 1;
diff --git a/examples/milestone/Bank/Bank.juvix b/examples/milestone/Bank/Bank.juvix
index 53c1af72aa..dd32abb508 100644
--- a/examples/milestone/Bank/Bank.juvix
+++ b/examples/milestone/Bank/Bank.juvix
@@ -6,8 +6,6 @@ module Bank;
 import Stdlib.Prelude open;
 import Stdlib.Debug.Fail open;
 
-import Stdlib.Data.Nat.Ord open;
-
 import Stdlib.Data.Nat as Nat;
 
 Address : Type := Nat;
diff --git a/examples/milestone/Collatz/Collatz.juvix b/examples/milestone/Collatz/Collatz.juvix
index 7977b9c715..6cb4a4e012 100644
--- a/examples/milestone/Collatz/Collatz.juvix
+++ b/examples/milestone/Collatz/Collatz.juvix
@@ -1,7 +1,6 @@
 module Collatz;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 collatzNext (n : Nat) : Nat :=
   if (mod n 2 == 0) (div n 2) (3 * n + 1);
diff --git a/examples/milestone/TicTacToe/CLI/TicTacToe.juvix b/examples/milestone/TicTacToe/CLI/TicTacToe.juvix
index 45bb264044..c7ec9c37a9 100644
--- a/examples/milestone/TicTacToe/CLI/TicTacToe.juvix
+++ b/examples/milestone/TicTacToe/CLI/TicTacToe.juvix
@@ -5,7 +5,6 @@
 --- The module Logic.Game contains the game logic.
 module CLI.TicTacToe;
 
-import Stdlib.Data.Nat.Ord open;
 import Stdlib.Prelude open;
 import Logic.Game open;
 
diff --git a/examples/milestone/TicTacToe/Logic/Extra.juvix b/examples/milestone/TicTacToe/Logic/Extra.juvix
index 98a7a06540..7d42d7ca29 100644
--- a/examples/milestone/TicTacToe/Logic/Extra.juvix
+++ b/examples/milestone/TicTacToe/Logic/Extra.juvix
@@ -1,7 +1,6 @@
 --- Some generic helper definitions.
 module Logic.Extra;
 
-import Stdlib.Data.Nat.Ord open;
 import Stdlib.Prelude open;
 
 --- Concatenates a list of strings
diff --git a/examples/milestone/TicTacToe/Logic/Game.juvix b/examples/milestone/TicTacToe/Logic/Game.juvix
index 01f8edd2a5..fc825929c9 100644
--- a/examples/milestone/TicTacToe/Logic/Game.juvix
+++ b/examples/milestone/TicTacToe/Logic/Game.juvix
@@ -4,7 +4,6 @@
 --- diagonal row is the winner. It is a solved game, with a forced draw assuming best play from both players.
 module Logic.Game;
 
-import Stdlib.Data.Nat.Ord open;
 import Stdlib.Prelude open;
 import Logic.Extra open public;
 import Logic.Board open public;
diff --git a/examples/milestone/TicTacToe/Logic/Square.juvix b/examples/milestone/TicTacToe/Logic/Square.juvix
index 710e8c4922..cb51144f57 100644
--- a/examples/milestone/TicTacToe/Logic/Square.juvix
+++ b/examples/milestone/TicTacToe/Logic/Square.juvix
@@ -2,7 +2,6 @@ module Logic.Square;
 
 import Stdlib.Prelude open;
 import Logic.Symbol open;
-import Stdlib.Data.Nat.Ord open;
 import Logic.Extra open;
 
 --- A square is each of the holes in a board
@@ -24,9 +23,5 @@ showSquare : Square → String
   | (occupied s) := " " ++str showSymbol s ++str " ";
 
 replace (player : Symbol) (k : Nat) : Square → Square
-  | (empty n) :=
-    if
-      (n Stdlib.Data.Nat.Ord.== k)
-      (occupied player)
-      (empty n)
+  | (empty n) := if (n == k) (occupied player) (empty n)
   | s := s;
diff --git a/examples/milestone/Tutorial/Tutorial.juvix b/examples/milestone/Tutorial/Tutorial.juvix
index 830a496e40..8d3d26c570 100644
--- a/examples/milestone/Tutorial/Tutorial.juvix
+++ b/examples/milestone/Tutorial/Tutorial.juvix
@@ -5,7 +5,5 @@ module Tutorial;
 
 -- import the standard library prelude and bring it into scope
 import Stdlib.Prelude open;
--- bring comparison operators on Nat into scope
-import Stdlib.Data.Nat.Ord open;
 
 main : IO := printStringLn "Hello world!";
diff --git a/juvix-stdlib b/juvix-stdlib
index adf58a7180..9a091c5453 160000
--- a/juvix-stdlib
+++ b/juvix-stdlib
@@ -1 +1 @@
-Subproject commit adf58a7180b361a022fb53c22ad9e5274ebf6f66
+Subproject commit 9a091c5453594ac66b3b25cde0c11a54a255a9c9
diff --git a/src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs b/src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs
index bd84143c40..4f45714103 100644
--- a/src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs
+++ b/src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs
@@ -58,7 +58,7 @@ fromCore :: Core.InfoTable -> (Morphism, Object)
 fromCore tab = case tab ^. Core.infoMain of
   Just sym ->
     let node = Core.lookupIdentifierNode tab sym
-        syms = reverse $ filter (/= sym) $ Core.createIdentDependencyInfo tab ^. Core.depInfoTopSort
+        syms = reverse $ filter (/= sym) $ Core.createCallGraph tab ^. Core.depInfoTopSort
         idents = map (Core.lookupIdentifierInfo tab) syms
         morph = run . runReader emptyEnv $ goIdents node idents
         obj = convertType $ Info.getNodeType node
diff --git a/src/Juvix/Compiler/Core/Data/IdentDependencyInfo.hs b/src/Juvix/Compiler/Core/Data/IdentDependencyInfo.hs
index 7ea3c88660..1267ffed28 100644
--- a/src/Juvix/Compiler/Core/Data/IdentDependencyInfo.hs
+++ b/src/Juvix/Compiler/Core/Data/IdentDependencyInfo.hs
@@ -1,5 +1,6 @@
 module Juvix.Compiler.Core.Data.IdentDependencyInfo where
 
+import Data.HashMap.Strict qualified as HashMap
 import Data.HashSet qualified as HashSet
 import Juvix.Compiler.Core.Data.InfoTable
 import Juvix.Compiler.Core.Extra.Utils
@@ -9,8 +10,8 @@ import Juvix.Compiler.Core.Language
 type IdentDependencyInfo = DependencyInfo Symbol
 
 -- | Compute the call graph
-createIdentDependencyInfo :: InfoTable -> IdentDependencyInfo
-createIdentDependencyInfo tab = createDependencyInfo graph startVertices
+createCallGraph :: InfoTable -> IdentDependencyInfo
+createCallGraph tab = createDependencyInfo graph startVertices
   where
     graph :: HashMap Symbol (HashSet Symbol)
     graph =
@@ -27,5 +28,28 @@ createIdentDependencyInfo tab = createDependencyInfo graph startVertices
     syms :: [Symbol]
     syms = maybe [] singleton (tab ^. infoMain)
 
+createSymbolDependencyInfo :: InfoTable -> IdentDependencyInfo
+createSymbolDependencyInfo tab = createDependencyInfo graph startVertices
+  where
+    graph :: HashMap Symbol (HashSet Symbol)
+    graph =
+      fmap
+        ( \IdentifierInfo {..} ->
+            getSymbols tab (lookupIdentifierNode tab _identifierSymbol)
+        )
+        (tab ^. infoIdentifiers)
+        <> foldr
+          ( \ConstructorInfo {..} ->
+              HashMap.insert _constructorInductive (getSymbols tab _constructorType)
+          )
+          mempty
+          (tab ^. infoConstructors)
+
+    startVertices :: HashSet Symbol
+    startVertices = HashSet.fromList syms
+
+    syms :: [Symbol]
+    syms = maybe [] singleton (tab ^. infoMain)
+
 recursiveIdents :: InfoTable -> HashSet Symbol
-recursiveIdents = nodesOnCycles . createIdentDependencyInfo
+recursiveIdents = nodesOnCycles . createCallGraph
diff --git a/src/Juvix/Compiler/Core/Data/InfoTable.hs b/src/Juvix/Compiler/Core/Data/InfoTable.hs
index d735297aa8..b1a6d16677 100644
--- a/src/Juvix/Compiler/Core/Data/InfoTable.hs
+++ b/src/Juvix/Compiler/Core/Data/InfoTable.hs
@@ -209,20 +209,33 @@ filterByFile f t =
     matchesLocation :: Maybe Location -> Bool
     matchesLocation l = l ^? _Just . intervalFile == Just f
 
--- | Prunes the orphaned entries of identMap and indentContext, i.e., ones that
--- have no corresponding entries in infoIdentifiers or infoInductives
+-- | Prunes the orphaned entries of identMap, indentContext and
+-- infoConstructors, i.e., ones that have no corresponding entries in
+-- infoIdentifiers or infoInductives
 pruneInfoTable :: InfoTable -> InfoTable
 pruneInfoTable tab =
-  over
-    identMap
-    ( HashMap.filter
-        ( \case
-            IdentFun s -> HashMap.member s (tab ^. infoIdentifiers)
-            IdentInd s -> HashMap.member s (tab ^. infoInductives)
-            IdentConstr tag -> HashMap.member tag (tab ^. infoConstructors)
-        )
-    )
+  pruneIdentMap
+    $ over
+      infoConstructors
+      ( HashMap.filter
+          ( \ConstructorInfo {..} ->
+              HashMap.member _constructorInductive (tab ^. infoInductives)
+          )
+      )
     $ over
       identContext
       (HashMap.filterWithKey (\s _ -> HashMap.member s (tab ^. infoIdentifiers)))
       tab
+  where
+    pruneIdentMap :: InfoTable -> InfoTable
+    pruneIdentMap tab' =
+      over
+        identMap
+        ( HashMap.filter
+            ( \case
+                IdentFun s -> HashMap.member s (tab' ^. infoIdentifiers)
+                IdentInd s -> HashMap.member s (tab' ^. infoInductives)
+                IdentConstr tag -> HashMap.member tag (tab' ^. infoConstructors)
+            )
+        )
+        tab'
diff --git a/src/Juvix/Compiler/Core/Data/TransformationId.hs b/src/Juvix/Compiler/Core/Data/TransformationId.hs
index a5a405ebef..431098a07f 100644
--- a/src/Juvix/Compiler/Core/Data/TransformationId.hs
+++ b/src/Juvix/Compiler/Core/Data/TransformationId.hs
@@ -26,6 +26,7 @@ data TransformationId
   | LambdaFolding
   | LetHoisting
   | Inlining
+  | MandatoryInlining
   | FoldTypeSynonyms
   | CaseCallLifting
   | SimplifyIfs
@@ -75,7 +76,7 @@ toNormalizeTransformations :: [TransformationId]
 toNormalizeTransformations = toEvalTransformations ++ [LetRecLifting, LetFolding, UnrollRecursion]
 
 toVampIRTransformations :: [TransformationId]
-toVampIRTransformations = toEvalTransformations ++ [CheckVampIR, LetRecLifting, OptPhaseVampIR, UnrollRecursion, Normalize, LetHoisting]
+toVampIRTransformations = toEvalTransformations ++ [FilterUnreachable, CheckVampIR, LetRecLifting, OptPhaseVampIR, UnrollRecursion, Normalize, LetHoisting]
 
 toStrippedTransformations :: [TransformationId]
 toStrippedTransformations =
diff --git a/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs b/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs
index 38be2e6e89..37803a7add 100644
--- a/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs
+++ b/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs
@@ -86,6 +86,7 @@ transformationText = \case
   LambdaFolding -> strLambdaFolding
   LetHoisting -> strLetHoisting
   Inlining -> strInlining
+  MandatoryInlining -> strMandatoryInlining
   FoldTypeSynonyms -> strFoldTypeSynonyms
   CaseCallLifting -> strCaseCallLifting
   SimplifyIfs -> strSimplifyIfs
@@ -191,6 +192,9 @@ strLambdaFolding = "lambda-folding"
 strInlining :: Text
 strInlining = "inlining"
 
+strMandatoryInlining :: Text
+strMandatoryInlining = "mandatory-inlining"
+
 strFoldTypeSynonyms :: Text
 strFoldTypeSynonyms = "fold-type-synonyms"
 
diff --git a/src/Juvix/Compiler/Core/Evaluator.hs b/src/Juvix/Compiler/Core/Evaluator.hs
index c7c3380359..edd6bd803a 100644
--- a/src/Juvix/Compiler/Core/Evaluator.hs
+++ b/src/Juvix/Compiler/Core/Evaluator.hs
@@ -89,7 +89,7 @@ geval opts herr ctx env0 = eval' env0
           Closure env' (NLam (Lambda i' bi b)) ->
             let !v = eval' env r in evalBody i' bi env' v b
           lv
-            | opts ^. evalOptionsNormalize ->
+            | opts ^. evalOptionsNormalize || opts ^. evalOptionsNoFailure ->
                 let !v = eval' env r in goNormApp i lv v
             | otherwise ->
                 evalError "invalid application" (mkApp i lv (substEnv env r))
@@ -106,7 +106,7 @@ geval opts herr ctx env0 = eval' env0
           NCtr (Constr _ tag args) ->
             branch n env args tag def bs
           v'
-            | opts ^. evalOptionsNormalize ->
+            | opts ^. evalOptionsNormalize || opts ^. evalOptionsNoFailure ->
                 goNormCase env i sym v' bs def
             | otherwise ->
                 evalError "matching on non-data" (substEnv env (mkCase i sym v' bs def))
@@ -214,7 +214,7 @@ geval opts herr ctx env0 = eval' env0
                 (Just v1, Just v2) ->
                   toNode (v1 `op` v2)
                 _
-                  | opts ^. evalOptionsNormalize ->
+                  | opts ^. evalOptionsNormalize || opts ^. evalOptionsNoFailure ->
                       mkBuiltinApp' opcode [vl, vr]
                   | otherwise ->
                       evalError "wrong operand type" n
diff --git a/src/Juvix/Compiler/Core/Extra/Utils.hs b/src/Juvix/Compiler/Core/Extra/Utils.hs
index b6c4e649e0..7dbcda3b84 100644
--- a/src/Juvix/Compiler/Core/Extra/Utils.hs
+++ b/src/Juvix/Compiler/Core/Extra/Utils.hs
@@ -144,6 +144,9 @@ nodeIdents f = ufoldA reassemble go
       NIdt i -> NIdt <$> f i
       n -> pure n
 
+getInductives :: Node -> HashSet Symbol
+getInductives n = HashSet.fromList (n ^.. nodeInductives)
+
 nodeInductives :: Traversal' Node Symbol
 nodeInductives f = ufoldA reassemble go
   where
@@ -151,6 +154,19 @@ nodeInductives f = ufoldA reassemble go
       NTyp ty -> NTyp <$> traverseOf typeConstrSymbol f ty
       n -> pure n
 
+getSymbols :: InfoTable -> Node -> HashSet Symbol
+getSymbols tab = gather go mempty
+  where
+    go :: HashSet Symbol -> Node -> HashSet Symbol
+    go acc = \case
+      NTyp TypeConstr {..} -> HashSet.insert _typeConstrSymbol acc
+      NIdt Ident {..} -> HashSet.insert _identSymbol acc
+      NCase Case {..} -> HashSet.insert _caseInductive acc
+      NCtr Constr {..}
+        | Just ci <- lookupConstructorInfo' tab _constrTag ->
+            HashSet.insert (ci ^. constructorInductive) acc
+      _ -> acc
+
 -- | Prism for NRec
 _NRec :: SimpleFold Node LetRec
 _NRec f = \case
diff --git a/src/Juvix/Compiler/Core/Transformation.hs b/src/Juvix/Compiler/Core/Transformation.hs
index f654221465..dd223b2004 100644
--- a/src/Juvix/Compiler/Core/Transformation.hs
+++ b/src/Juvix/Compiler/Core/Transformation.hs
@@ -35,6 +35,7 @@ import Juvix.Compiler.Core.Transformation.Optimize.FilterUnreachable (filterUnre
 import Juvix.Compiler.Core.Transformation.Optimize.Inlining
 import Juvix.Compiler.Core.Transformation.Optimize.LambdaFolding
 import Juvix.Compiler.Core.Transformation.Optimize.LetFolding
+import Juvix.Compiler.Core.Transformation.Optimize.MandatoryInlining
 import Juvix.Compiler.Core.Transformation.Optimize.Phase.Eval qualified as Phase.Eval
 import Juvix.Compiler.Core.Transformation.Optimize.Phase.Exec qualified as Phase.Exec
 import Juvix.Compiler.Core.Transformation.Optimize.Phase.Geb qualified as Phase.Geb
@@ -74,6 +75,7 @@ applyTransformations ts tbl = foldM (flip appTrans) tbl ts
       LambdaFolding -> return . lambdaFolding
       LetHoisting -> return . letHoisting
       Inlining -> inlining
+      MandatoryInlining -> return . mandatoryInlining
       FoldTypeSynonyms -> return . foldTypeSynonyms
       CaseCallLifting -> return . caseCallLifting
       SimplifyIfs -> return . simplifyIfs
diff --git a/src/Juvix/Compiler/Core/Transformation/LetHoisting.hs b/src/Juvix/Compiler/Core/Transformation/LetHoisting.hs
index 47373b0844..59d5188461 100644
--- a/src/Juvix/Compiler/Core/Transformation/LetHoisting.hs
+++ b/src/Juvix/Compiler/Core/Transformation/LetHoisting.hs
@@ -1,4 +1,4 @@
--- Moves al let expressions at the top, just after the top lambdas. This
+-- Moves all let expressions at the top, just after the top lambdas. This
 -- transformation assumes:
 -- - There are no LetRecs, Lambdas (other than the ones at the top), nor Match.
 -- - Case nodes do not have binders.
diff --git a/src/Juvix/Compiler/Core/Transformation/Optimize/FilterUnreachable.hs b/src/Juvix/Compiler/Core/Transformation/Optimize/FilterUnreachable.hs
index a1e165217c..c9a2d1e4f9 100644
--- a/src/Juvix/Compiler/Core/Transformation/Optimize/FilterUnreachable.hs
+++ b/src/Juvix/Compiler/Core/Transformation/Optimize/FilterUnreachable.hs
@@ -5,10 +5,13 @@ import Juvix.Compiler.Core.Data.IdentDependencyInfo
 import Juvix.Compiler.Core.Transformation.Base
 
 filterUnreachable :: InfoTable -> InfoTable
-filterUnreachable tab = pruneInfoTable $ over infoIdentifiers goFilter tab
+filterUnreachable tab =
+  pruneInfoTable $
+    over infoInductives goFilter $
+      over infoIdentifiers goFilter tab
   where
-    depInfo = createIdentDependencyInfo tab
+    depInfo = createSymbolDependencyInfo tab
 
-    goFilter :: HashMap Symbol IdentifierInfo -> HashMap Symbol IdentifierInfo
-    goFilter idents =
-      HashMap.filterWithKey (\sym _ -> isReachable depInfo sym) idents
+    goFilter :: HashMap Symbol a -> HashMap Symbol a
+    goFilter =
+      HashMap.filterWithKey (\sym _ -> isReachable depInfo sym)
diff --git a/src/Juvix/Compiler/Core/Transformation/Optimize/Inlining.hs b/src/Juvix/Compiler/Core/Transformation/Optimize/Inlining.hs
index aca760e230..9874fc73e3 100644
--- a/src/Juvix/Compiler/Core/Transformation/Optimize/Inlining.hs
+++ b/src/Juvix/Compiler/Core/Transformation/Optimize/Inlining.hs
@@ -32,6 +32,8 @@ convertNode inlineDepth recSyms tab = dmapL go
                   Just (InlinePartiallyApplied k)
                     | length args >= k ->
                         mkApps def args
+                  Just InlineAlways ->
+                    mkApps def args
                   Just InlineNever ->
                     node
                   _
@@ -48,6 +50,17 @@ convertNode inlineDepth recSyms tab = dmapL go
                   def = lookupIdentifierNode tab _identSymbol
               _ ->
                 node
+      NIdt Ident {..} ->
+        case pi of
+          Just InlineFullyApplied | argsNum == 0 -> def
+          Just (InlinePartiallyApplied 0) -> def
+          Just InlineAlways -> def
+          _ -> node
+        where
+          ii = lookupIdentifierInfo tab _identSymbol
+          pi = ii ^. identifierPragmas . pragmasInline
+          argsNum = ii ^. identifierArgsNum
+          def = lookupIdentifierNode tab _identSymbol
       -- inline zero-argument definitions automatically if inlining would result
       -- in case reduction
       NCase cs@Case {..} -> case _caseValue of
diff --git a/src/Juvix/Compiler/Core/Transformation/Optimize/MandatoryInlining.hs b/src/Juvix/Compiler/Core/Transformation/Optimize/MandatoryInlining.hs
new file mode 100644
index 0000000000..96b6b32848
--- /dev/null
+++ b/src/Juvix/Compiler/Core/Transformation/Optimize/MandatoryInlining.hs
@@ -0,0 +1,18 @@
+module Juvix.Compiler.Core.Transformation.Optimize.MandatoryInlining where
+
+import Juvix.Compiler.Core.Extra
+import Juvix.Compiler.Core.Transformation.Base
+
+convertNode :: InfoTable -> Node -> Node
+convertNode tab = dmap go
+  where
+    go :: Node -> Node
+    go node = case node of
+      NIdt Ident {..}
+        | Just InlineAlways <- lookupIdentifierInfo tab _identSymbol ^. identifierPragmas . pragmasInline ->
+            lookupIdentifierNode tab _identSymbol
+      _ ->
+        node
+
+mandatoryInlining :: InfoTable -> InfoTable
+mandatoryInlining tab = mapAllNodes (convertNode tab) tab
diff --git a/src/Juvix/Compiler/Core/Transformation/Optimize/Phase/Eval.hs b/src/Juvix/Compiler/Core/Transformation/Optimize/Phase/Eval.hs
index ad8553740d..d0153e4ba4 100644
--- a/src/Juvix/Compiler/Core/Transformation/Optimize/Phase/Eval.hs
+++ b/src/Juvix/Compiler/Core/Transformation/Optimize/Phase/Eval.hs
@@ -1,11 +1,15 @@
 module Juvix.Compiler.Core.Transformation.Optimize.Phase.Eval where
 
-import Juvix.Compiler.Core.Options
 import Juvix.Compiler.Core.Transformation.Base
+import Juvix.Compiler.Core.Transformation.Optimize.CaseFolding
 import Juvix.Compiler.Core.Transformation.Optimize.LambdaFolding
 import Juvix.Compiler.Core.Transformation.Optimize.LetFolding
+import Juvix.Compiler.Core.Transformation.Optimize.MandatoryInlining
 
-optimize :: (Member (Reader CoreOptions) r) => InfoTable -> Sem r InfoTable
+optimize :: InfoTable -> Sem r InfoTable
 optimize =
-  withOptimizationLevel 1 $
-    return . letFolding . lambdaFolding
+  return
+    . caseFolding
+    . letFolding
+    . lambdaFolding
+    . mandatoryInlining
diff --git a/src/Juvix/Compiler/Core/Transformation/UnrollRecursion.hs b/src/Juvix/Compiler/Core/Transformation/UnrollRecursion.hs
index 50acfd7d83..26a89b0d5b 100644
--- a/src/Juvix/Compiler/Core/Transformation/UnrollRecursion.hs
+++ b/src/Juvix/Compiler/Core/Transformation/UnrollRecursion.hs
@@ -13,7 +13,7 @@ unrollRecursion tab = do
   (mp, tab') <-
     runState @(HashMap Symbol Symbol) mempty $
       execInfoTableBuilder tab $
-        forM_ (buildSCCs (createIdentDependencyInfo tab)) goSCC
+        forM_ (buildSCCs (createCallGraph tab)) goSCC
   return $ mapIdentSymbols mp $ pruneInfoTable tab'
   where
     mapIdentSymbols :: HashMap Symbol Symbol -> InfoTable -> InfoTable
diff --git a/src/Juvix/Compiler/Internal/Extra.hs b/src/Juvix/Compiler/Internal/Extra.hs
index 28cfe72cd7..f0ac2101ad 100644
--- a/src/Juvix/Compiler/Internal/Extra.hs
+++ b/src/Juvix/Compiler/Internal/Extra.hs
@@ -93,7 +93,7 @@ genFieldProjection _funDefName info fieldIx = do
         _funDefTerminating = False,
         _funDefInstance = False,
         _funDefBuiltin = Nothing,
-        _funDefPragmas = mempty,
+        _funDefPragmas = mempty {_pragmasInline = Just InlineAlways},
         _funDefBody = body',
         _funDefType = foldFunType (inductiveArgs ++ [saturatedTy]) retTy,
         ..
diff --git a/src/Juvix/Data/Pragmas.hs b/src/Juvix/Data/Pragmas.hs
index d6d2b0ab25..8a21f73f16 100644
--- a/src/Juvix/Data/Pragmas.hs
+++ b/src/Juvix/Data/Pragmas.hs
@@ -5,7 +5,8 @@ import Juvix.Data.Yaml
 import Juvix.Prelude.Base
 
 data PragmaInline
-  = InlineNever
+  = InlineAlways
+  | InlineNever
   | InlineFullyApplied
   | InlinePartiallyApplied {_pragmaInlineArgsNum :: Int}
   deriving stock (Show, Eq, Ord, Data, Generic)
@@ -116,7 +117,7 @@ instance FromJSON Pragmas where
         return Pragmas {..}
 
       parseInline :: Parse YamlError PragmaInline
-      parseInline = parseInlineArgsNum Aeson.<|> parseInlineBool
+      parseInline = parseInlineArgsNum Aeson.<|> parseInlineBool Aeson.<|> parseInlineAlwaysNever
         where
           parseInlineArgsNum :: Parse YamlError PragmaInline
           parseInlineArgsNum = do
@@ -128,6 +129,14 @@ instance FromJSON Pragmas where
             b <- asBool
             (if b then return InlineFullyApplied else return InlineNever)
 
+          parseInlineAlwaysNever :: Parse YamlError PragmaInline
+          parseInlineAlwaysNever = do
+            txt <- asText
+            case txt of
+              "always" -> return InlineAlways
+              "never" -> return InlineNever
+              _ -> throwCustomError ("unrecognized inline specification: " <> txt)
+
       parseUnroll :: Parse YamlError PragmaUnroll
       parseUnroll = do
         _pragmaUnrollDepth <- asIntegral
@@ -209,6 +218,7 @@ instance Monoid Pragmas where
 adjustPragmaInline :: Int -> PragmaInline -> PragmaInline
 adjustPragmaInline n = \case
   InlinePartiallyApplied k -> InlinePartiallyApplied (k + n)
+  InlineAlways -> InlineAlways
   InlineNever -> InlineNever
   InlineFullyApplied -> InlineFullyApplied
 
diff --git a/test/Core/Transformation/Unrolling.hs b/test/Core/Transformation/Unrolling.hs
index d1b3aba181..3215553afa 100644
--- a/test/Core/Transformation/Unrolling.hs
+++ b/test/Core/Transformation/Unrolling.hs
@@ -44,5 +44,5 @@ liftTest _testEval =
 checkNoRecursion :: InfoTable -> Assertion
 checkNoRecursion tab =
   when
-    (isCyclic (createIdentDependencyInfo tab))
+    (isCyclic (createCallGraph tab))
     (assertFailure "recursion detected")
diff --git a/tests/Compilation/positive/test006.juvix b/tests/Compilation/positive/test006.juvix
index 4a9b1c8ecb..0aa53d89d4 100644
--- a/tests/Compilation/positive/test006.juvix
+++ b/tests/Compilation/positive/test006.juvix
@@ -2,7 +2,6 @@
 module test006;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 terminating
 loop : Nat := loop;
diff --git a/tests/Compilation/positive/test012.juvix b/tests/Compilation/positive/test012.juvix
index 43e068d45f..66839cd96f 100644
--- a/tests/Compilation/positive/test012.juvix
+++ b/tests/Compilation/positive/test012.juvix
@@ -2,7 +2,6 @@
 module test012;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 type Tree :=
   | leaf : Tree
diff --git a/tests/Compilation/positive/test013.juvix b/tests/Compilation/positive/test013.juvix
index e9d84dc4d4..97a7fa90e8 100644
--- a/tests/Compilation/positive/test013.juvix
+++ b/tests/Compilation/positive/test013.juvix
@@ -2,7 +2,6 @@
 module test013;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 f : Nat → Nat → Nat
   | x :=
diff --git a/tests/Compilation/positive/test015.juvix b/tests/Compilation/positive/test015.juvix
index 85ac0d1035..d02d8e912f 100644
--- a/tests/Compilation/positive/test015.juvix
+++ b/tests/Compilation/positive/test015.juvix
@@ -2,7 +2,6 @@
 module test015;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 terminating
 f : Nat → Nat → Nat
diff --git a/tests/Compilation/positive/test020.juvix b/tests/Compilation/positive/test020.juvix
index 9a387d19ba..339977e2a1 100644
--- a/tests/Compilation/positive/test020.juvix
+++ b/tests/Compilation/positive/test020.juvix
@@ -2,7 +2,6 @@
 module test020;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 -- McCarthy's 91 function
 terminating
diff --git a/tests/Compilation/positive/test021.juvix b/tests/Compilation/positive/test021.juvix
index ac7ce1afcc..a0fbbff074 100644
--- a/tests/Compilation/positive/test021.juvix
+++ b/tests/Compilation/positive/test021.juvix
@@ -2,7 +2,6 @@
 module test021;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 terminating
 power' : Nat → Nat → Nat → Nat
diff --git a/tests/Compilation/positive/test022.juvix b/tests/Compilation/positive/test022.juvix
index 8a30c42d33..a2f69854f5 100644
--- a/tests/Compilation/positive/test022.juvix
+++ b/tests/Compilation/positive/test022.juvix
@@ -2,7 +2,6 @@
 module test022;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 gen : Nat → List Nat
   | zero := nil
diff --git a/tests/Compilation/positive/test023.juvix b/tests/Compilation/positive/test023.juvix
index fdfb1af8e7..63a6ba24fa 100644
--- a/tests/Compilation/positive/test023.juvix
+++ b/tests/Compilation/positive/test023.juvix
@@ -2,11 +2,10 @@
 module test023;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 terminating
 f : Nat → Nat
-  
+
   | x := if (x < 1) 1 (2 * x + g (sub x 1));
 
 terminating
diff --git a/tests/Compilation/positive/test025.juvix b/tests/Compilation/positive/test025.juvix
index a40bddc0a8..e7e1280945 100644
--- a/tests/Compilation/positive/test025.juvix
+++ b/tests/Compilation/positive/test025.juvix
@@ -2,7 +2,6 @@
 module test025;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 terminating
 gcd : Nat → Nat → Nat
diff --git a/tests/Compilation/positive/test028.juvix b/tests/Compilation/positive/test028.juvix
index 2d8002728f..6f9e9b9b88 100644
--- a/tests/Compilation/positive/test028.juvix
+++ b/tests/Compilation/positive/test028.juvix
@@ -2,7 +2,6 @@
 module test028;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 type Stream :=
   | cons : Nat → (Unit → Stream) → Stream;
diff --git a/tests/Compilation/positive/test032.juvix b/tests/Compilation/positive/test032.juvix
index bdf8495c00..775f0a8ecd 100644
--- a/tests/Compilation/positive/test032.juvix
+++ b/tests/Compilation/positive/test032.juvix
@@ -2,7 +2,6 @@
 module test032;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 split : {A : Type} → Nat → List A → List A × List A
   | zero xs := nil, xs
diff --git a/tests/Compilation/positive/test034.juvix b/tests/Compilation/positive/test034.juvix
index d12f4f9db4..6658f44e2b 100644
--- a/tests/Compilation/positive/test034.juvix
+++ b/tests/Compilation/positive/test034.juvix
@@ -2,7 +2,6 @@
 module test034;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 sum : Nat → Nat :=
   let
diff --git a/tests/Compilation/positive/test049.juvix b/tests/Compilation/positive/test049.juvix
index 3ccfc19fe9..f916e7ca8c 100644
--- a/tests/Compilation/positive/test049.juvix
+++ b/tests/Compilation/positive/test049.juvix
@@ -1,9 +1,7 @@
 -- Builtin Int
 module test049;
 
-import Stdlib.Prelude open hiding {+; *; div; mod};
-import Stdlib.Data.Int.Ord open;
-import Stdlib.Data.Int open;
+import Stdlib.Prelude open;
 
 f : Int -> Nat
   | (negSuc n) := n
@@ -23,8 +21,8 @@ main : IO :=
     >> printBoolLn (-1 == -2)
     >> printBoolLn (-1 == -1)
     >> printBoolLn (1 == 1)
-    >> printBoolLn (-1 == 1)
-    >> printIntLn (-1 + 1)
+    >> printBoolLn (-1 == ofNat 1)
+    >> printIntLn (-1 + ofNat 1)
     >> printIntLn (negNat (suc zero))
     >> printIntLn
       (let
@@ -35,9 +33,9 @@ main : IO :=
       (let
         g : Int -> Int := neg;
       in g -1)
-    >> printIntLn (-2 * 2)
-    >> printIntLn (div 4 -2)
-    >> printIntLn (2 - 2)
+    >> printIntLn (-2 * ofNat 2)
+    >> printIntLn (div (ofNat 4) -2)
+    >> printIntLn (ofNat 2 - ofNat 2)
     >> printBoolLn (nonNeg 0)
     >> printBoolLn (nonNeg -1)
     >> printIntLn (mod -5 -2)
@@ -45,5 +43,5 @@ main : IO :=
     >> printBoolLn (0 <= 0)
     >> printBoolLn (0 < 1)
     >> printBoolLn (1 <= 0)
-    >> printIntLn (mod 5 -3)
-    >> printIntLn (div 5 -3);
+    >> printIntLn (mod (ofNat 5) -3)
+    >> printIntLn (div (ofNat 5) -3);
diff --git a/tests/Compilation/positive/test050.juvix b/tests/Compilation/positive/test050.juvix
index 8617f407a5..0543155f0a 100644
--- a/tests/Compilation/positive/test050.juvix
+++ b/tests/Compilation/positive/test050.juvix
@@ -1,13 +1,11 @@
 -- Pattern matching with integers
 module test050;
 
-import Stdlib.Prelude open hiding {+; *; div; mod};
-import Stdlib.Data.Int.Ord open;
-import Stdlib.Data.Int open;
+import Stdlib.Prelude open;
 
 f : Int -> Int
   | (negSuc zero) := ofNat 0
   | (negSuc m@(suc n)) := ofNat n + ofNat m
-  | (ofNat n) := neg (ofNat n - 7);
+  | (ofNat n) := neg (ofNat n - ofNat 7);
 
 main : Int := f -10 - f 1 + f -1;
diff --git a/tests/Geb/positive/Compilation/test010.juvix b/tests/Geb/positive/Compilation/test010.juvix
index 6fc6e284cd..7db0cb4278 100644
--- a/tests/Geb/positive/Compilation/test010.juvix
+++ b/tests/Geb/positive/Compilation/test010.juvix
@@ -2,7 +2,6 @@
 module test010;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 f : Nat → Nat → Nat
   | x :=
diff --git a/tests/Geb/positive/Compilation/test012.juvix b/tests/Geb/positive/Compilation/test012.juvix
index 3adf746083..0c6b89a08b 100644
--- a/tests/Geb/positive/Compilation/test012.juvix
+++ b/tests/Geb/positive/Compilation/test012.juvix
@@ -2,7 +2,6 @@
 module test012;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 pow0 : Nat := 1;
 
diff --git a/tests/Geb/positive/Compilation/test016.juvix b/tests/Geb/positive/Compilation/test016.juvix
index 63a3359e3a..3913c04c45 100644
--- a/tests/Geb/positive/Compilation/test016.juvix
+++ b/tests/Geb/positive/Compilation/test016.juvix
@@ -2,7 +2,6 @@
 module test016;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 terminating
 f : Nat → Nat → Nat
diff --git a/tests/Geb/positive/Compilation/test020.juvix b/tests/Geb/positive/Compilation/test020.juvix
index 19d8b8649e..0fd6c4a35a 100644
--- a/tests/Geb/positive/Compilation/test020.juvix
+++ b/tests/Geb/positive/Compilation/test020.juvix
@@ -2,7 +2,6 @@
 module test020;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 terminating
 f91 : Nat → Nat
diff --git a/tests/Geb/positive/Compilation/test021.juvix b/tests/Geb/positive/Compilation/test021.juvix
index 524a0ca5f9..7ea78c4c43 100644
--- a/tests/Geb/positive/Compilation/test021.juvix
+++ b/tests/Geb/positive/Compilation/test021.juvix
@@ -2,7 +2,6 @@
 module test021;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 terminating
 power' : Nat → Nat → Nat → Nat
diff --git a/tests/Geb/positive/Compilation/test022.juvix b/tests/Geb/positive/Compilation/test022.juvix
index c076b5102a..9a1df8e3cc 100644
--- a/tests/Geb/positive/Compilation/test022.juvix
+++ b/tests/Geb/positive/Compilation/test022.juvix
@@ -2,11 +2,9 @@
 module test022;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 terminating
 f : Nat → Nat
-  
   | x := if (x < 1) 1 (2 * x + g (sub x 1));
 
 terminating
diff --git a/tests/Geb/positive/Compilation/test023.juvix b/tests/Geb/positive/Compilation/test023.juvix
index dc99f21d3c..49e4bc26a5 100644
--- a/tests/Geb/positive/Compilation/test023.juvix
+++ b/tests/Geb/positive/Compilation/test023.juvix
@@ -2,7 +2,6 @@
 module test023;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 terminating
 gcd : Nat → Nat → Nat
diff --git a/tests/Geb/positive/Compilation/test025.juvix b/tests/Geb/positive/Compilation/test025.juvix
index 69d4235623..83b1077aad 100644
--- a/tests/Geb/positive/Compilation/test025.juvix
+++ b/tests/Geb/positive/Compilation/test025.juvix
@@ -2,7 +2,6 @@
 module test025;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 pow : Nat -> Nat
   | zero := 1
diff --git a/tests/Geb/positive/Compilation/test026.juvix b/tests/Geb/positive/Compilation/test026.juvix
index 183aeed7d7..7d052f7c69 100644
--- a/tests/Geb/positive/Compilation/test026.juvix
+++ b/tests/Geb/positive/Compilation/test026.juvix
@@ -2,7 +2,6 @@
 module test026;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 sum : Nat → Nat :=
   let
diff --git a/tests/Internal/Core/positive/test006.juvix b/tests/Internal/Core/positive/test006.juvix
index 07314796a3..19be5d2551 100644
--- a/tests/Internal/Core/positive/test006.juvix
+++ b/tests/Internal/Core/positive/test006.juvix
@@ -1,7 +1,6 @@
 module test006;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 terminating
 loop : Nat := loop;
diff --git a/tests/Internal/Core/positive/test011.juvix b/tests/Internal/Core/positive/test011.juvix
index b5fcf61dd6..4cd1e42a6c 100644
--- a/tests/Internal/Core/positive/test011.juvix
+++ b/tests/Internal/Core/positive/test011.juvix
@@ -1,7 +1,6 @@
 module test011;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 fib' : Nat -> Nat -> Nat -> Nat
   | zero x _ := x
diff --git a/tests/Internal/positive/QuickSort.juvix b/tests/Internal/positive/QuickSort.juvix
index ebfc46f4ac..65c6318b9b 100644
--- a/tests/Internal/positive/QuickSort.juvix
+++ b/tests/Internal/positive/QuickSort.juvix
@@ -1,7 +1,6 @@
 module QuickSort;
 
 import Stdlib.Prelude open hiding {quickSort};
-import Stdlib.Data.Nat.Ord open;
 
 qsHelper : {A : Type} → A → List A × List A → List A
   | a (l, r) := l ++ (a :: nil) ++ r;
@@ -40,6 +39,5 @@ four : Nat := suc three;
 
 main : List Nat :=
   uniq
-    compare
-    (quickSort compare (flatten (gen2 three four nil)));
-
+    Ord.cmp
+    (quickSort Ord.cmp (flatten (gen2 three four nil)));
diff --git a/tests/VampIR/negative/test001.juvix b/tests/VampIR/negative/test001.juvix
index 630445caf3..82571509cc 100644
--- a/tests/VampIR/negative/test001.juvix
+++ b/tests/VampIR/negative/test001.juvix
@@ -1,7 +1,6 @@
 module test001;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 {-# argnames: [a, b
                 c] #-}
diff --git a/tests/VampIR/positive/Compilation/test001.juvix b/tests/VampIR/positive/Compilation/test001.juvix
index bc2fa5d2eb..69320a4ad3 100644
--- a/tests/VampIR/positive/Compilation/test001.juvix
+++ b/tests/VampIR/positive/Compilation/test001.juvix
@@ -2,7 +2,6 @@
 module test001;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 main : Nat -> Nat
   | x := if (x == 0) 1 0;
diff --git a/tests/VampIR/positive/Compilation/test002.juvix b/tests/VampIR/positive/Compilation/test002.juvix
index 4aeeb46b17..b925d7c767 100644
--- a/tests/VampIR/positive/Compilation/test002.juvix
+++ b/tests/VampIR/positive/Compilation/test002.juvix
@@ -2,7 +2,6 @@
 module test002;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 type optbool :=
   | Just : Bool -> optbool
diff --git a/tests/VampIR/positive/Compilation/test003.juvix b/tests/VampIR/positive/Compilation/test003.juvix
index 575840e407..c41e34aba1 100644
--- a/tests/VampIR/positive/Compilation/test003.juvix
+++ b/tests/VampIR/positive/Compilation/test003.juvix
@@ -2,7 +2,6 @@
 module test003;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 type enum :=
   | opt0 : enum
diff --git a/tests/VampIR/positive/Compilation/test006.juvix b/tests/VampIR/positive/Compilation/test006.juvix
index c1ce191f60..bcf541d587 100644
--- a/tests/VampIR/positive/Compilation/test006.juvix
+++ b/tests/VampIR/positive/Compilation/test006.juvix
@@ -2,7 +2,6 @@
 module test006;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 type enum :=
   | opt0 : enum
diff --git a/tests/VampIR/positive/Compilation/test008.juvix b/tests/VampIR/positive/Compilation/test008.juvix
index ba643ef029..e048afd352 100644
--- a/tests/VampIR/positive/Compilation/test008.juvix
+++ b/tests/VampIR/positive/Compilation/test008.juvix
@@ -2,7 +2,6 @@
 module test008;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 f : Nat → Nat → Nat
   | x :=
diff --git a/tests/VampIR/positive/Compilation/test010.juvix b/tests/VampIR/positive/Compilation/test010.juvix
index d7b2a64867..199fd2abb0 100644
--- a/tests/VampIR/positive/Compilation/test010.juvix
+++ b/tests/VampIR/positive/Compilation/test010.juvix
@@ -2,7 +2,6 @@
 module test010;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 pow0 : Nat := 1;
 
diff --git a/tests/VampIR/positive/Compilation/test017.juvix b/tests/VampIR/positive/Compilation/test017.juvix
index c13b853682..6851afc7a9 100644
--- a/tests/VampIR/positive/Compilation/test017.juvix
+++ b/tests/VampIR/positive/Compilation/test017.juvix
@@ -2,7 +2,6 @@
 module test017;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 {-# unroll: 11 #-}
 terminating
diff --git a/tests/VampIR/positive/Compilation/test018.juvix b/tests/VampIR/positive/Compilation/test018.juvix
index 9724065eaf..e8c6f310af 100644
--- a/tests/VampIR/positive/Compilation/test018.juvix
+++ b/tests/VampIR/positive/Compilation/test018.juvix
@@ -2,7 +2,6 @@
 module test018;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 pow : Nat -> Nat
   | zero := 1
diff --git a/tests/VampIR/positive/Compilation/test021.juvix b/tests/VampIR/positive/Compilation/test021.juvix
index 5bdba00afe..b288a2cbe7 100644
--- a/tests/VampIR/positive/Compilation/test021.juvix
+++ b/tests/VampIR/positive/Compilation/test021.juvix
@@ -2,7 +2,6 @@
 module test021;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 power : Nat → Nat → Nat :=
   let
diff --git a/tests/VampIR/positive/Compilation/test022.juvix b/tests/VampIR/positive/Compilation/test022.juvix
index 7105ee3a2e..83323e2943 100644
--- a/tests/VampIR/positive/Compilation/test022.juvix
+++ b/tests/VampIR/positive/Compilation/test022.juvix
@@ -2,7 +2,6 @@
 module test022;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 power : Nat → Nat → Nat :=
   let
diff --git a/tests/VampIR/positive/Compilation/test023.juvix b/tests/VampIR/positive/Compilation/test023.juvix
index 14e6adaff4..66dc355067 100644
--- a/tests/VampIR/positive/Compilation/test023.juvix
+++ b/tests/VampIR/positive/Compilation/test023.juvix
@@ -2,7 +2,6 @@
 module test023;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 main : Nat → Nat → Nat
   | x y :=
diff --git a/tests/benchmark/ackermann/juvix/ackermann.juvix b/tests/benchmark/ackermann/juvix/ackermann.juvix
index 48ecdace3f..3f6258829b 100644
--- a/tests/benchmark/ackermann/juvix/ackermann.juvix
+++ b/tests/benchmark/ackermann/juvix/ackermann.juvix
@@ -2,7 +2,6 @@
 module ackermann;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 iter : {A : Type} → (A → A) → Nat → A → A
   | f zero := id
diff --git a/tests/benchmark/combinations/juvix/combinations.juvix b/tests/benchmark/combinations/juvix/combinations.juvix
index 6a3c752b64..0691f84d6d 100644
--- a/tests/benchmark/combinations/juvix/combinations.juvix
+++ b/tests/benchmark/combinations/juvix/combinations.juvix
@@ -2,7 +2,6 @@
 module combinations;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 terminating
 go : Nat → Nat → Nat
diff --git a/tests/benchmark/cps/juvix/cps.juvix b/tests/benchmark/cps/juvix/cps.juvix
index 9942c7fb29..b5a0f8b8a8 100644
--- a/tests/benchmark/cps/juvix/cps.juvix
+++ b/tests/benchmark/cps/juvix/cps.juvix
@@ -2,7 +2,6 @@
 module cps;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 step : Nat → Nat → Nat → (Nat → Nat → Nat → Nat) → Nat
   | zero n _ _ := n
diff --git a/tests/benchmark/fibonacci/juvix/fibonacci.juvix b/tests/benchmark/fibonacci/juvix/fibonacci.juvix
index f4d3419f1a..de3685c373 100644
--- a/tests/benchmark/fibonacci/juvix/fibonacci.juvix
+++ b/tests/benchmark/fibonacci/juvix/fibonacci.juvix
@@ -2,7 +2,6 @@
 module fibonacci;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 go : Nat → Nat → Nat → Nat
   | zero n _ := n
diff --git a/tests/benchmark/fold/juvix/fold.juvix b/tests/benchmark/fold/juvix/fold.juvix
index 51f2d3a978..62a9330388 100644
--- a/tests/benchmark/fold/juvix/fold.juvix
+++ b/tests/benchmark/fold/juvix/fold.juvix
@@ -2,7 +2,6 @@
 module fold;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 plusMod : Nat → Nat → Nat
   | x y := mod (x + y) 268435456;
diff --git a/tests/benchmark/mapfold/juvix/mapfold.juvix b/tests/benchmark/mapfold/juvix/mapfold.juvix
index 247e1ae7a3..26db7626ed 100644
--- a/tests/benchmark/mapfold/juvix/mapfold.juvix
+++ b/tests/benchmark/mapfold/juvix/mapfold.juvix
@@ -2,7 +2,6 @@
 module mapfold;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 run : Nat → Nat → List Nat → Nat
   | zero acc lst := acc
diff --git a/tests/benchmark/maybe/juvix/maybe.juvix b/tests/benchmark/maybe/juvix/maybe.juvix
index c7670662d2..6f8dd620f8 100644
--- a/tests/benchmark/maybe/juvix/maybe.juvix
+++ b/tests/benchmark/maybe/juvix/maybe.juvix
@@ -2,7 +2,6 @@
 module maybe;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 type Tree :=
   | leaf : Tree
diff --git a/tests/benchmark/mergesort/juvix/mergesort.juvix b/tests/benchmark/mergesort/juvix/mergesort.juvix
index 7acc9bae2b..b1126319c9 100644
--- a/tests/benchmark/mergesort/juvix/mergesort.juvix
+++ b/tests/benchmark/mergesort/juvix/mergesort.juvix
@@ -2,7 +2,6 @@
 module mergesort;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 split_go
   : {A : Type} → List A → List A → List A → List A × List A
diff --git a/tests/benchmark/prime/juvix/prime.juvix b/tests/benchmark/prime/juvix/prime.juvix
index 0c505b3f53..c21efb74cf 100644
--- a/tests/benchmark/prime/juvix/prime.juvix
+++ b/tests/benchmark/prime/juvix/prime.juvix
@@ -2,7 +2,6 @@
 module prime;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 checkDivisible : Nat → List Nat → Bool
   | p nil := false
diff --git a/tests/positive/Format.juvix b/tests/positive/Format.juvix
index 9865cc1bfe..9b0951f177 100644
--- a/tests/positive/Format.juvix
+++ b/tests/positive/Format.juvix
@@ -12,8 +12,6 @@ hiding -- Hide some names
 -- Bool either
 Bool; true; false; mkShow; module Show};
 
-import Stdlib.Data.Nat.Ord open;
-
 -- Lorem ipsum dolor sit amet, consectetur adipiscing elit
 terminating
 -- Comment between terminating and type sig
diff --git a/tests/positive/issue1731/builtinTrace.juvix b/tests/positive/issue1731/builtinTrace.juvix
index f1a0740186..66882db661 100644
--- a/tests/positive/issue1731/builtinTrace.juvix
+++ b/tests/positive/issue1731/builtinTrace.juvix
@@ -1,7 +1,6 @@
 module builtinTrace;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 builtin trace
 axiom trace : {A : Type} → A → A;
diff --git a/tests/smoke/Commands/dev/core.smoke.yaml b/tests/smoke/Commands/dev/core.smoke.yaml
index 6fdc638f5e..3baf2ca089 100644
--- a/tests/smoke/Commands/dev/core.smoke.yaml
+++ b/tests/smoke/Commands/dev/core.smoke.yaml
@@ -62,6 +62,7 @@ tests:
       - dev
       - core
       - from-concrete
+      - -t eta-expand-apps
       - --normalize
     args:
       - positive/Internal/Norm.juvix
diff --git a/tests/smoke/Commands/repl.smoke.yaml b/tests/smoke/Commands/repl.smoke.yaml
index 9678ba15b5..f2e32c621e 100644
--- a/tests/smoke/Commands/repl.smoke.yaml
+++ b/tests/smoke/Commands/repl.smoke.yaml
@@ -74,11 +74,7 @@ tests:
     stdin: ":def + (+) (((+)))"
     stdout:
       contains: |
-        --- Addition for ;Nat;s.
-        builtin nat-plus
-        + : Nat → Nat → Nat
-          | zero b := b
-          | (suc a) b := suc (a + b)
+        + {A} {{Natural A}} : A -> A -> A := Natural.+
     exit-status: 0
 
   - name: repl-def-infix
@@ -89,11 +85,7 @@ tests:
     stdin: ":def +"
     stdout:
       contains: |
-        --- Addition for ;Nat;s.
-        builtin nat-plus
-        + : Nat → Nat → Nat
-          | zero b := b
-          | (suc a) b := suc (a + b)
+        + {A} {{Natural A}} : A -> A -> A := Natural.+
     exit-status: 0
 
   - name: open
@@ -454,7 +446,7 @@ tests:
     command:
       - juvix
       - repl
-    stdin: "import Stdlib.Data.Int.Ord as Int open\n1 == 1"
+    stdin: "import Stdlib.Data.Int.Ord as Int open\n1 Int.== 1"
     stdout:
       contains: "true"
     exit-status: 0
@@ -463,9 +455,9 @@ tests:
     command:
       - juvix
       - repl
-    stdin: "import Stdlib.Data.Int.Ord open\n1 == 1"
+    stdin: "import Stdlib.Data.Int.Ord open\ncompare 1 1"
     stdout:
-      contains: "true"
+      contains: "EQ"
     exit-status: 0
 
   - name: infix-constructors