diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 723cb958c8..47bea9ccee 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -17,14 +17,6 @@ concurrency:
   cancel-in-progress: true
 
 jobs:
-  not-a-draft:
-    runs-on: ubuntu-latest
-    if: github.event.pull_request.draft == true
-    steps:
-      - name: Fails in order to indicate that pull request needs to be marked as
-              ready to review.
-        run: exit 1
-
   docs:
     if: github.event.pull_request.merged == true
     runs-on: ubuntu-latest
@@ -55,7 +47,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v2
-      - uses: mrkkrp/ormolu-action@v5
+      - uses: mrkkrp/ormolu-action@v6
         with:
           extra-args: >-
             --ghc-opt -XDerivingStrategies
diff --git a/app/Commands/Compile.hs b/app/Commands/Compile.hs
index 1085b71ba7..97597f860c 100644
--- a/app/Commands/Compile.hs
+++ b/app/Commands/Compile.hs
@@ -109,10 +109,13 @@ prepareRuntime projRoot o = do
     libCRuntimeDir :: [(FilePath, BS.ByteString)]
     libCRuntimeDir = $(FE.makeRelativeToProject "minic-runtime/libc" >>= FE.embedDir)
 
+    builtinCRuntimeDir :: [(FilePath, BS.ByteString)]
+    builtinCRuntimeDir = $(FE.makeRelativeToProject "minic-runtime/builtins" >>= FE.embedDir)
+
     runtimeProjectDir :: [(FilePath, BS.ByteString)]
     runtimeProjectDir = case o ^. compileRuntime of
-      RuntimeStandalone -> standaloneRuntimeDir
-      RuntimeLibC -> libCRuntimeDir
+      RuntimeStandalone -> standaloneRuntimeDir <> builtinCRuntimeDir
+      RuntimeLibC -> libCRuntimeDir <> builtinCRuntimeDir
 
     writeRuntime :: (FilePath, BS.ByteString) -> IO ()
     writeRuntime (filePath, contents) =
diff --git a/docs/org/notes/builtins.org b/docs/org/notes/builtins.org
new file mode 100644
index 0000000000..265c4ab79c
--- /dev/null
+++ b/docs/org/notes/builtins.org
@@ -0,0 +1,70 @@
+#+title: Builtins
+#+author: Jan Mas Rovira
+
+* Overview
+
+The goal is to support builtin types and functions that get compiled to
+efficient primitives. We plan on supporting primitives for the following types
+of definitions:
+
+1. Builtin inductive definitions. For example:
+   #+begin_example
+   builtin natural
+   inductive Nat {
+     zero : Nat;
+     suc : Nat → Nat;
+   };
+   #+end_example
+   We will call this the canonical definition of natural numbers.
+
+2. Builtin function definitions. For example:
+   #+begin_src text
+   inifl 6 +;
+   builtin natural-plus
+   + : Nat → Nat → Nat;
+   + zero b ≔ b;
+   + (suc a) b ≔ suc (a + b);
+   #+end_src
+
+3. Builtin axiom definitions. For example:
+   #+begin_src text
+   builtin natural-print
+   axiom printNat : Nat → Action;
+   #+end_src
+
+** Collecting builtin information
+
+The idea is that builtin definitions are treated normally throughout the
+pipeline except in the backend part. There is one exception to that. We need to
+collect information about the builtins that have been included in the code and
+what are the terms that refer to them. For instance, imagine that we find this
+definitions in a minijuvix module:
+#+begin_src text
+builtin natural
+inductive MyNat {
+    z : MyNat;
+    s : MyNat → MyNat;
+};
+#+end_src
+We need to take care of the following:
+1. Check that the definition =MyInt= is up to renaming equal to the canonical
+   definition that we provide in the compiler.
+2. Rember a map from concrete to canonical names: {MyNat ↦ Nat; z ↦ zero; s ↦ suc};
+3. Rembember that we have a definition for builtin natural numbers. This is
+   necessary if later we attempt to define a builtin function or axiom that
+   depends on natural numbers.
+
+
+In the compiler we need to know the following:
+1. For inductives:
+   1. What is the primitive type that we will target in the backend: E.g. {Nat ↦ int}.
+   2. For constructors:
+      1. What is the primitive constructor function: E.g. {zero ↦ 0; suc ↦ plus_one};
+      2. How to test if a term matches a pattern with that constructor.
+         E.g. {zero ↦ is_zero; suc ↦ is_not_zero};
+      3. How to deconstruct/project each of the constructor arguments. E.g. {zero ↦
+         ∅; suc ↦ minus_one}}. Note that if a constructor takes multiple arguments
+         we will need to have a projection function for each argument.
+2. For functions and axioms:
+   1. What is the primitive function that we will target in the backend: E.g. {+
+      ↦ add}.
diff --git a/minic-runtime/builtins/io.h b/minic-runtime/builtins/io.h
new file mode 100644
index 0000000000..7954bdee56
--- /dev/null
+++ b/minic-runtime/builtins/io.h
@@ -0,0 +1,10 @@
+#ifndef IO_H_
+#define IO_H_
+
+typedef int prim_io;
+
+prim_io prim_sequence(prim_io a, prim_io b) {
+    return a + b;
+}
+
+#endif // IO_H_
diff --git a/minic-runtime/builtins/nat.h b/minic-runtime/builtins/nat.h
new file mode 100644
index 0000000000..260e954f13
--- /dev/null
+++ b/minic-runtime/builtins/nat.h
@@ -0,0 +1,31 @@
+#ifndef NAT_H_
+#define NAT_H_
+
+#include <stdbool.h>
+
+typedef int prim_nat;
+
+#define prim_zero 0
+
+prim_nat prim_suc(prim_nat n) {
+    return n + 1;
+}
+
+bool is_prim_zero(prim_nat n) {
+    return n == 0;
+}
+
+bool is_prim_suc(prim_nat n) {
+    return n != 0;
+}
+
+prim_nat proj_ca0_prim_suc(prim_nat n) {
+    return n - 1;
+}
+
+prim_nat prim_natplus(prim_nat a, prim_nat b) {
+    return a + b;
+}
+
+
+#endif // NAT_H_
diff --git a/minic-runtime/libc/minic-runtime.h b/minic-runtime/libc/minic-runtime.h
index 7a390b7b3c..dd1e92e1fe 100644
--- a/minic-runtime/libc/minic-runtime.h
+++ b/minic-runtime/libc/minic-runtime.h
@@ -5,6 +5,9 @@
 #include <stdio.h>
 #include <string.h>
 
+#include "nat.h"
+#include "io.h"
+
 typedef __UINTPTR_TYPE__ uintptr_t;
 
 typedef struct minijuvix_function {
@@ -90,4 +93,8 @@ int putStrLn(const char* str) {
     return fflush(stdout);
 }
 
+prim_io prim_printNat(prim_nat n) {
+    return putStrLn(intToStr(n));
+}
+
 #endif // MINIC_RUNTIME_H_
diff --git a/minic-runtime/standalone/minic-runtime.h b/minic-runtime/standalone/minic-runtime.h
index a82750c4b7..6b0fd89595 100644
--- a/minic-runtime/standalone/minic-runtime.h
+++ b/minic-runtime/standalone/minic-runtime.h
@@ -1,6 +1,9 @@
 #ifndef MINIC_RUNTIME_H_
 #define MINIC_RUNTIME_H_
 
+#include "nat.h"
+#include "io.h"
+
 typedef __SIZE_TYPE__ size_t;
 typedef __UINT8_TYPE__ uint8_t;
 typedef __UINT16_TYPE__ uint16_t;
@@ -182,6 +185,10 @@ int putStrLn(const char* str) {
     return putStr(str) || putStr("\n");
 }
 
+prim_io prim_printNat(prim_nat n) {
+    return putStrLn(intToStr(n));
+}
+
 // Tries to parse str as a positive integer.
 // Returns -1 if parsing fails.
 int parsePositiveInt(char *str) {
diff --git a/src/MiniJuvix/Builtins.hs b/src/MiniJuvix/Builtins.hs
new file mode 100644
index 0000000000..95aedf0e63
--- /dev/null
+++ b/src/MiniJuvix/Builtins.hs
@@ -0,0 +1,10 @@
+module MiniJuvix.Builtins
+  ( module MiniJuvix.Builtins.Effect,
+    module MiniJuvix.Builtins.Natural,
+    module MiniJuvix.Builtins.IO,
+  )
+where
+
+import MiniJuvix.Builtins.Effect
+import MiniJuvix.Builtins.IO
+import MiniJuvix.Builtins.Natural
diff --git a/src/MiniJuvix/Builtins/Base.hs b/src/MiniJuvix/Builtins/Base.hs
new file mode 100644
index 0000000000..90bdbb0cf0
--- /dev/null
+++ b/src/MiniJuvix/Builtins/Base.hs
@@ -0,0 +1,30 @@
+module MiniJuvix.Builtins.Base
+  ( module MiniJuvix.Builtins.Base,
+  )
+where
+
+import MiniJuvix.Internal.Strings qualified as Str
+import MiniJuvix.Prelude
+import MiniJuvix.Prelude.Pretty
+
+data BuiltinsEnum
+  = BuiltinsNatural
+  | BuiltinsZero
+  | BuiltinsSuc
+  | BuiltinsNaturalPlus
+  | BuiltinsNaturalPrint
+  | BuiltinsIO
+  | BuiltinsIOSequence
+  deriving stock (Show, Eq, Generic)
+
+instance Hashable BuiltinsEnum
+
+instance Pretty BuiltinsEnum where
+  pretty = \case
+    BuiltinsNatural -> Str.natural
+    BuiltinsZero -> "zero"
+    BuiltinsSuc -> "suc"
+    BuiltinsNaturalPlus -> Str.naturalPlus
+    BuiltinsNaturalPrint -> Str.naturalPrint
+    BuiltinsIO -> Str.io
+    BuiltinsIOSequence -> Str.ioSequence
diff --git a/src/MiniJuvix/Builtins/Effect.hs b/src/MiniJuvix/Builtins/Effect.hs
new file mode 100644
index 0000000000..17b1596881
--- /dev/null
+++ b/src/MiniJuvix/Builtins/Effect.hs
@@ -0,0 +1,64 @@
+module MiniJuvix.Builtins.Effect
+  ( module MiniJuvix.Builtins.Effect,
+  )
+where
+
+import MiniJuvix.Builtins.Error
+import MiniJuvix.Prelude
+import MiniJuvix.Syntax.Abstract.Language.Extra
+
+data Builtins m a where
+  GetBuiltinName' :: Interval -> BuiltinPrim -> Builtins m Name
+  -- GetBuiltin :: Name -> Builtins m (Maybe BuiltinPrims)
+  RegisterBuiltin' :: BuiltinPrim -> Name -> Builtins m ()
+
+makeSem ''Builtins
+
+registerBuiltin :: (IsBuiltin a, Member Builtins r) => a -> Name -> Sem r ()
+registerBuiltin = registerBuiltin' . toBuiltinPrim
+
+getBuiltinName :: (IsBuiltin a, Member Builtins r) => Interval -> a -> Sem r Name
+getBuiltinName i = getBuiltinName' i . toBuiltinPrim
+
+data BuiltinsState = BuiltinsState
+  { _builtinsTable :: HashMap BuiltinPrim Name,
+    _builtinsNameTable :: HashMap Name BuiltinPrim
+  }
+
+makeLenses ''BuiltinsState
+
+iniState :: BuiltinsState
+iniState = BuiltinsState mempty mempty
+
+re :: forall r a. Member (Error MiniJuvixError) r => Sem (Builtins ': r) a -> Sem (State BuiltinsState ': r) a
+re = reinterpret $ \case
+  GetBuiltinName' i b -> fromMaybeM notDefined (gets (^. builtinsTable . at b))
+    where
+      notDefined :: Sem (State BuiltinsState : r) x
+      notDefined =
+        throw $
+          MiniJuvixError
+            NotDefined
+              { _notDefinedBuiltin = b,
+                _notDefinedLoc = i
+              }
+  -- GetBuiltin n -> gets (^. builtinsNameTable . at n)
+  RegisterBuiltin' b n -> do
+    s <- gets (^. builtinsTable . at b)
+    case s of
+      Nothing -> do
+        modify (over builtinsTable (set (at b) (Just n)))
+        modify (over builtinsNameTable (set (at n) (Just b)))
+      Just {} -> alreadyDefined
+    where
+      alreadyDefined :: Sem (State BuiltinsState : r) x
+      alreadyDefined =
+        throw $
+          MiniJuvixError
+            AlreadyDefined
+              { _alreadyDefinedBuiltin = b,
+                _alreadyDefinedLoc = getLoc n
+              }
+
+runBuiltins :: Member (Error MiniJuvixError) r => Sem (Builtins ': r) a -> Sem r a
+runBuiltins = evalState iniState . re
diff --git a/src/MiniJuvix/Builtins/Error.hs b/src/MiniJuvix/Builtins/Error.hs
new file mode 100644
index 0000000000..d6e997d613
--- /dev/null
+++ b/src/MiniJuvix/Builtins/Error.hs
@@ -0,0 +1,45 @@
+module MiniJuvix.Builtins.Error where
+
+import MiniJuvix.Prelude
+import MiniJuvix.Prelude.Pretty
+import MiniJuvix.Syntax.Concrete.Builtins
+import MiniJuvix.Termination.Error.Pretty
+
+data AlreadyDefined = AlreadyDefined
+  { _alreadyDefinedBuiltin :: BuiltinPrim,
+    _alreadyDefinedLoc :: Interval
+  }
+
+makeLenses ''AlreadyDefined
+
+hh :: Doc Eann -> Doc Eann
+hh = annotate Highlight
+
+instance ToGenericError AlreadyDefined where
+  genericError e =
+    GenericError
+      { _genericErrorLoc = i,
+        _genericErrorMessage = prettyError msg,
+        _genericErrorIntervals = [i]
+      }
+    where
+      i = e ^. alreadyDefinedLoc
+      msg = "The builtin" <+> hh (pretty (e ^. alreadyDefinedBuiltin)) <+> "has already been defined"
+
+data NotDefined = NotDefined
+  { _notDefinedBuiltin :: BuiltinPrim,
+    _notDefinedLoc :: Interval
+  }
+
+makeLenses ''NotDefined
+
+instance ToGenericError NotDefined where
+  genericError e =
+    GenericError
+      { _genericErrorLoc = i,
+        _genericErrorMessage = prettyError msg,
+        _genericErrorIntervals = [i]
+      }
+    where
+      i = e ^. notDefinedLoc
+      msg = "The builtin" <+> hh (pretty (e ^. notDefinedBuiltin)) <+> "has not been defined"
diff --git a/src/MiniJuvix/Builtins/IO.hs b/src/MiniJuvix/Builtins/IO.hs
new file mode 100644
index 0000000000..3184f06a91
--- /dev/null
+++ b/src/MiniJuvix/Builtins/IO.hs
@@ -0,0 +1,16 @@
+module MiniJuvix.Builtins.IO where
+
+import MiniJuvix.Builtins.Effect
+import MiniJuvix.Prelude
+import MiniJuvix.Syntax.Abstract.Language.Extra
+
+registerIO :: Member Builtins r => AxiomDef -> Sem r ()
+registerIO d = do
+  unless (d ^. axiomType === smallUniverse) (error "IO should be in the small universe")
+  registerBuiltin BuiltinIO (d ^. axiomName)
+
+registerIOSequence :: Member Builtins r => AxiomDef -> Sem r ()
+registerIOSequence d = do
+  io <- getBuiltinName (getLoc d) BuiltinIO
+  unless (d ^. axiomType === (io --> io --> io)) (error "IO sequence have type IO → IO")
+  registerBuiltin BuiltinIOSequence (d ^. axiomName)
diff --git a/src/MiniJuvix/Builtins/Natural.hs b/src/MiniJuvix/Builtins/Natural.hs
new file mode 100644
index 0000000000..c32765d6dd
--- /dev/null
+++ b/src/MiniJuvix/Builtins/Natural.hs
@@ -0,0 +1,69 @@
+module MiniJuvix.Builtins.Natural where
+
+import Data.HashSet qualified as HashSet
+import MiniJuvix.Builtins.Effect
+import MiniJuvix.Internal.NameIdGen
+import MiniJuvix.Prelude
+import MiniJuvix.Syntax.Abstract.Language.Extra
+import MiniJuvix.Syntax.Abstract.Pretty
+
+registerNaturalDef :: Member Builtins r => InductiveDef -> Sem r ()
+registerNaturalDef d = do
+  unless (null (d ^. inductiveParameters)) (error "Naturals should have no type parameters")
+  unless (d ^. inductiveType === smallUniverse) (error "Naturals should be in the small universe")
+  registerBuiltin BuiltinNatural (d ^. inductiveName)
+  case d ^. inductiveConstructors of
+    [c1, c2] -> registerZero c1 >> registerSuc c2
+    _ -> error "Natural numbers should have exactly two constructors"
+
+registerZero :: Member Builtins r => InductiveConstructorDef -> Sem r ()
+registerZero d@(InductiveConstructorDef zero ty) = do
+  nat <- getBuiltinName (getLoc d) BuiltinNatural
+  unless (ty === nat) (error $ "zero has the wrong type " <> ppSimple ty <> " | " <> ppSimple nat)
+  registerBuiltin BuiltinNaturalZero zero
+
+registerSuc :: Member Builtins r => InductiveConstructorDef -> Sem r ()
+registerSuc d@(InductiveConstructorDef suc ty) = do
+  nat <- getBuiltinName (getLoc d) BuiltinNatural
+  unless (ty === (nat --> nat)) (error "suc has the wrong type")
+  registerBuiltin BuiltinNaturalSuc suc
+
+registerNaturalPrint :: Members '[Builtins] r => AxiomDef -> Sem r ()
+registerNaturalPrint f = do
+  nat <- getBuiltinName (getLoc f) BuiltinNatural
+  io <- getBuiltinName (getLoc f) BuiltinIO
+  unless (f ^. axiomType === (nat --> io)) (error "Natural print has the wrong type signature")
+  registerBuiltin BuiltinNaturalPrint (f ^. axiomName)
+
+registerNaturalPlus :: Members '[Builtins, NameIdGen] r => FunctionDef -> Sem r ()
+registerNaturalPlus f = do
+  nat <- getBuiltinName (getLoc f) BuiltinNatural
+  zero <- toExpression <$> getBuiltinName (getLoc f) BuiltinNaturalZero
+  suc <- toExpression <$> getBuiltinName (getLoc f) BuiltinNaturalSuc
+  let plus = f ^. funDefName
+      ty = f ^. funDefTypeSig
+  unless (ty === (nat --> nat --> nat)) (error "Natural plus has the wrong type signature")
+  registerBuiltin BuiltinNaturalPlus plus
+  varn <- freshVar "n"
+  varm <- freshVar "m"
+  let n = toExpression varn
+      m = toExpression varm
+      freeVars = HashSet.fromList [varn, varm]
+      a =% b = (a ==% b) freeVars
+      (.+.) :: (IsExpression a, IsExpression b) => a -> b -> Expression
+      x .+. y = plus @@ x @@ y
+      exClauses :: [(Expression, Expression)]
+      exClauses =
+        [ (zero .+. m, m),
+          ((suc @@ n) .+. m, suc @@ (n .+. m))
+        ]
+      clauses :: [(Expression, Expression)]
+      clauses =
+        [ (clauseLhsAsExpression c, c ^. clauseBody)
+          | c <- toList (f ^. funDefClauses)
+        ]
+  case zipExactMay exClauses clauses of
+    Nothing -> error "Natural plus has the wrong number of clauses"
+    Just z -> forM_ z $ \((exLhs, exBody), (lhs, body)) -> do
+      unless (exLhs =% lhs) (error "clause lhs does not match")
+      unless (exBody =% body) (error $ "clause body does not match " <> ppSimple exBody <> " | " <> ppSimple body)
diff --git a/src/MiniJuvix/Internal/Strings.hs b/src/MiniJuvix/Internal/Strings.hs
index f21a5393c9..399498f86b 100644
--- a/src/MiniJuvix/Internal/Strings.hs
+++ b/src/MiniJuvix/Internal/Strings.hs
@@ -80,6 +80,24 @@ error = "error"
 string :: IsString s => s
 string = "string"
 
+natural :: IsString s => s
+natural = "natural"
+
+io :: IsString s => s
+io = "IO"
+
+ioSequence :: IsString s => s
+ioSequence = "IO-sequence"
+
+naturalPrint :: IsString s => s
+naturalPrint = "natural-print"
+
+naturalPlus :: IsString s => s
+naturalPlus = "natural-plus"
+
+builtin :: IsString s => s
+builtin = "builtin"
+
 type_ :: IsString s => s
 type_ = "Type"
 
diff --git a/src/MiniJuvix/Pipeline.hs b/src/MiniJuvix/Pipeline.hs
index aa2b3b55b2..79a9757fbf 100644
--- a/src/MiniJuvix/Pipeline.hs
+++ b/src/MiniJuvix/Pipeline.hs
@@ -4,6 +4,7 @@ module MiniJuvix.Pipeline
   )
 where
 
+import MiniJuvix.Builtins
 import MiniJuvix.Internal.NameIdGen
 import MiniJuvix.Pipeline.EntryPoint
 import MiniJuvix.Prelude
@@ -20,10 +21,10 @@ import MiniJuvix.Translation.MonoJuvixToMiniC qualified as MiniC
 import MiniJuvix.Translation.MonoJuvixToMiniHaskell qualified as MiniHaskell
 import MiniJuvix.Translation.ScopedToAbstract qualified as Abstract
 
-type PipelineEff = '[Files, NameIdGen, Error MiniJuvixError, Embed IO]
+type PipelineEff = '[Files, NameIdGen, Builtins, Error MiniJuvixError, Embed IO]
 
 runIOEither :: Sem PipelineEff a -> IO (Either MiniJuvixError a)
-runIOEither = runM . runError . runNameIdGen . runFilesIO
+runIOEither = runM . runError . runBuiltins . runNameIdGen . runFilesIO
 
 runIO :: Sem PipelineEff a -> IO a
 runIO = runIOEither >=> mayThrow
@@ -48,43 +49,43 @@ upToScoping ::
 upToScoping = upToParsing >=> pipelineScoper
 
 upToAbstract ::
-  Members '[Files, NameIdGen, Error MiniJuvixError] r =>
+  Members '[Files, NameIdGen, Builtins, Error MiniJuvixError] r =>
   EntryPoint ->
   Sem r Abstract.AbstractResult
 upToAbstract = upToScoping >=> pipelineAbstract
 
 upToMicroJuvix ::
-  Members '[Files, NameIdGen, Error MiniJuvixError] r =>
+  Members '[Files, NameIdGen, Builtins, Error MiniJuvixError] r =>
   EntryPoint ->
   Sem r MicroJuvix.MicroJuvixResult
 upToMicroJuvix = upToAbstract >=> pipelineMicroJuvix
 
 upToMicroJuvixArity ::
-  Members '[Files, NameIdGen, Error MiniJuvixError] r =>
+  Members '[Files, NameIdGen, Builtins, Error MiniJuvixError] r =>
   EntryPoint ->
   Sem r MicroJuvix.MicroJuvixArityResult
 upToMicroJuvixArity = upToMicroJuvix >=> pipelineMicroJuvixArity
 
 upToMicroJuvixTyped ::
-  Members '[Files, NameIdGen, Error MiniJuvixError] r =>
+  Members '[Files, NameIdGen, Builtins, Error MiniJuvixError] r =>
   EntryPoint ->
   Sem r MicroJuvix.MicroJuvixTypedResult
 upToMicroJuvixTyped = upToMicroJuvixArity >=> pipelineMicroJuvixTyped
 
 upToMonoJuvix ::
-  Members '[Files, NameIdGen, Error MiniJuvixError] r =>
+  Members '[Files, NameIdGen, Builtins, Error MiniJuvixError] r =>
   EntryPoint ->
   Sem r MonoJuvix.MonoJuvixResult
 upToMonoJuvix = upToMicroJuvixTyped >=> pipelineMonoJuvix
 
 upToMiniHaskell ::
-  Members '[Files, NameIdGen, Error MiniJuvixError] r =>
+  Members '[Files, NameIdGen, Builtins, Error MiniJuvixError] r =>
   EntryPoint ->
   Sem r MiniHaskell.MiniHaskellResult
 upToMiniHaskell = upToMonoJuvix >=> pipelineMiniHaskell
 
 upToMiniC ::
-  Members '[Files, NameIdGen, Error MiniJuvixError] r =>
+  Members '[Files, NameIdGen, Builtins, Error MiniJuvixError] r =>
   EntryPoint ->
   Sem r MiniC.MiniCResult
 upToMiniC = upToMonoJuvix >=> pipelineMiniC
@@ -104,7 +105,7 @@ pipelineScoper ::
 pipelineScoper = mapError (MiniJuvixError @Scoper.ScoperError) . Scoper.entryScoper
 
 pipelineAbstract ::
-  Members '[Error MiniJuvixError] r =>
+  Members '[Error MiniJuvixError, Builtins, NameIdGen] r =>
   Scoper.ScoperResult ->
   Sem r Abstract.AbstractResult
 pipelineAbstract = mapError (MiniJuvixError @Scoper.ScoperError) . Abstract.entryAbstract
@@ -140,6 +141,7 @@ pipelineMiniHaskell ::
 pipelineMiniHaskell = MiniHaskell.entryMiniHaskell
 
 pipelineMiniC ::
+  Member Builtins r =>
   MonoJuvix.MonoJuvixResult ->
   Sem r MiniC.MiniCResult
 pipelineMiniC = MiniC.entryMiniC
diff --git a/src/MiniJuvix/Prelude/Base.hs b/src/MiniJuvix/Prelude/Base.hs
index a386d289a0..0697be795a 100644
--- a/src/MiniJuvix/Prelude/Base.hs
+++ b/src/MiniJuvix/Prelude/Base.hs
@@ -3,6 +3,7 @@ module MiniJuvix.Prelude.Base
     module Control.Applicative,
     module Control.Monad.Extra,
     module Control.Monad.Fix,
+    module Data.Bitraversable,
     module Data.Bool,
     module Data.Char,
     module Data.Either.Extra,
@@ -45,6 +46,7 @@ module MiniJuvix.Prelude.Base
     module Polysemy.Output,
     module Polysemy.Reader,
     module Polysemy.State,
+    module Language.Haskell.TH.Syntax,
     module Prettyprinter,
     module System.Directory,
     module System.Exit,
@@ -68,6 +70,7 @@ import Control.Applicative
 import Control.Monad.Extra
 import Control.Monad.Fix
 import Data.Bifunctor hiding (first, second)
+import Data.Bitraversable
 import Data.Bool
 import Data.ByteString.Lazy (ByteString)
 import Data.Char
@@ -103,7 +106,7 @@ import Data.Maybe
 import Data.Monoid
 import Data.Ord
 import Data.Semigroup (Semigroup, (<>))
-import Data.Singletons
+import Data.Singletons hiding ((@@))
 import Data.Singletons.Sigma
 import Data.Singletons.TH (genSingletons, promoteOrdInstances, singOrdInstances)
 import Data.Stream (Stream)
@@ -122,6 +125,7 @@ import GHC.Generics (Generic)
 import GHC.Num
 import GHC.Real
 import GHC.Stack.Types
+import Language.Haskell.TH.Syntax (Lift)
 import Lens.Micro.Platform hiding (both, _head)
 import Polysemy
 import Polysemy.Embed
@@ -243,6 +247,9 @@ tableNestedInsert k1 k2 a = tableInsert (HashMap.singleton k2) (HashMap.insert k
 nonEmptyUnsnoc :: NonEmpty a -> (Maybe (NonEmpty a), a)
 nonEmptyUnsnoc e = (NonEmpty.nonEmpty (NonEmpty.init e), NonEmpty.last e)
 
+_nonEmpty :: Lens' [a] (Maybe (NonEmpty a))
+_nonEmpty f x = maybe [] toList <$> f (nonEmpty x)
+
 groupSortOn :: Ord b => (a -> b) -> [a] -> [NonEmpty a]
 groupSortOn f = map (fromJust . nonEmpty) . List.groupSortOn f
 
@@ -271,6 +278,13 @@ infixl 7 <+?>
 (<+?>) :: Doc ann -> Maybe (Doc ann) -> Doc ann
 (<+?>) a = maybe a (a <+>)
 
+infixl 7 <?+>
+
+(<?+>) :: Maybe (Doc ann) -> Doc ann -> Doc ann
+(<?+>) = \case
+  Nothing -> id
+  Just a -> (a <+>)
+
 infixl 7 <?>
 
 (<?>) :: Semigroup m => m -> Maybe m -> m
@@ -307,3 +321,6 @@ fromRightIO pp = fromRightIO' (putStrLn . pp)
 
 nubHashable :: Hashable a => [a] -> [a]
 nubHashable = HashSet.toList . HashSet.fromList
+
+allElements :: (Bounded a, Enum a) => [a]
+allElements = [minBound .. maxBound]
diff --git a/src/MiniJuvix/Prelude/Error/GenericError.hs b/src/MiniJuvix/Prelude/Error/GenericError.hs
index fd53e87d18..7993b00719 100644
--- a/src/MiniJuvix/Prelude/Error/GenericError.hs
+++ b/src/MiniJuvix/Prelude/Error/GenericError.hs
@@ -28,9 +28,10 @@ instance HasLoc GenericError where
 genericErrorHeader :: GenericError -> Doc a
 genericErrorHeader g =
   pretty (g ^. genericErrorLoc)
-    <> colon <+> "error"
     <> colon
-    <> line
+    <+> "error"
+      <> colon
+      <> line
 
 class ToGenericError a where
   genericError :: a -> GenericError
diff --git a/src/MiniJuvix/Prelude/Files.hs b/src/MiniJuvix/Prelude/Files.hs
index 67bde0cf37..83d1cdc3fe 100644
--- a/src/MiniJuvix/Prelude/Files.hs
+++ b/src/MiniJuvix/Prelude/Files.hs
@@ -26,7 +26,9 @@ runFilesPure fs = interpret $ \case
     Nothing ->
       error $
         pack $
-          "file " <> f <> " does not exist."
+          "file "
+            <> f
+            <> " does not exist."
             <> "\nThe contents of the mocked file system are:\n"
             <> unlines (HashMap.keys fs)
     Just c -> return c
diff --git a/src/MiniJuvix/Syntax/Abstract/Language.hs b/src/MiniJuvix/Syntax/Abstract/Language.hs
index 9e872cccc9..e5c86c1ebb 100644
--- a/src/MiniJuvix/Syntax/Abstract/Language.hs
+++ b/src/MiniJuvix/Syntax/Abstract/Language.hs
@@ -2,6 +2,9 @@ module MiniJuvix.Syntax.Abstract.Language
   ( module MiniJuvix.Syntax.Abstract.Language,
     module MiniJuvix.Syntax.Concrete.Language,
     module MiniJuvix.Syntax.Hole,
+    module MiniJuvix.Syntax.Concrete.Builtins,
+    module MiniJuvix.Syntax.Usage,
+    module MiniJuvix.Syntax.Universe,
     module MiniJuvix.Syntax.Abstract.Name,
     module MiniJuvix.Syntax.Wildcard,
     module MiniJuvix.Syntax.IsImplicit,
@@ -10,10 +13,12 @@ where
 
 import MiniJuvix.Prelude
 import MiniJuvix.Syntax.Abstract.Name
-import MiniJuvix.Syntax.Concrete.Language (BackendItem, ForeignBlock (..), LiteralLoc (..), Usage, symbolLoc)
+import MiniJuvix.Syntax.Concrete.Builtins
+import MiniJuvix.Syntax.Concrete.Language (BackendItem, ForeignBlock (..), LiteralLoc (..), symbolLoc)
 import MiniJuvix.Syntax.Hole
 import MiniJuvix.Syntax.IsImplicit
 import MiniJuvix.Syntax.Universe
+import MiniJuvix.Syntax.Usage
 import MiniJuvix.Syntax.Wildcard
 
 type LocalModule = Module
@@ -46,12 +51,14 @@ data FunctionDef = FunctionDef
   { _funDefName :: FunctionName,
     _funDefTypeSig :: Expression,
     _funDefClauses :: NonEmpty FunctionClause,
+    _funDefBuiltin :: Maybe BuiltinFunction,
     _funDefTerminating :: Bool
   }
   deriving stock (Eq, Show)
 
 data FunctionClause = FunctionClause
-  { _clausePatterns :: [Pattern],
+  { _clauseName :: FunctionName,
+    _clausePatterns :: [Pattern],
     _clauseBody :: Expression
   }
   deriving stock (Eq, Show)
@@ -170,8 +177,9 @@ data Pattern
 
 data InductiveDef = InductiveDef
   { _inductiveName :: InductiveName,
+    _inductiveBuiltin :: Maybe BuiltinInductive,
     _inductiveParameters :: [FunctionParameter],
-    _inductiveType :: Maybe Expression,
+    _inductiveType :: Expression,
     _inductiveConstructors :: [InductiveConstructorDef]
   }
   deriving stock (Eq, Show)
@@ -184,6 +192,7 @@ data InductiveConstructorDef = InductiveConstructorDef
 
 data AxiomDef = AxiomDef
   { _axiomName :: AxiomName,
+    _axiomBuiltin :: Maybe BuiltinAxiom,
     _axiomType :: Expression
   }
   deriving stock (Eq, Show)
@@ -202,3 +211,15 @@ makeLenses ''ConstructorRef
 makeLenses ''InductiveRef
 makeLenses ''AxiomRef
 makeLenses ''AxiomDef
+
+instance HasLoc InductiveConstructorDef where
+  getLoc = getLoc . (^. constructorName)
+
+instance HasLoc InductiveDef where
+  getLoc = getLoc . (^. inductiveName)
+
+instance HasLoc AxiomDef where
+  getLoc = getLoc . (^. axiomName)
+
+instance HasLoc FunctionDef where
+  getLoc = getLoc . (^. funDefName)
diff --git a/src/MiniJuvix/Syntax/Abstract/Language/Extra.hs b/src/MiniJuvix/Syntax/Abstract/Language/Extra.hs
index 31d8169af0..0f79620046 100644
--- a/src/MiniJuvix/Syntax/Abstract/Language/Extra.hs
+++ b/src/MiniJuvix/Syntax/Abstract/Language/Extra.hs
@@ -4,9 +4,19 @@ module MiniJuvix.Syntax.Abstract.Language.Extra
   )
 where
 
+import Data.HashMap.Strict qualified as HashMap
+import Data.HashSet qualified as HashSet
+import MiniJuvix.Internal.NameIdGen
 import MiniJuvix.Prelude
 import MiniJuvix.Syntax.Abstract.Language
 
+data ApplicationArg = ApplicationArg
+  { _appArgIsImplicit :: IsImplicit,
+    _appArg :: Expression
+  }
+
+makeLenses ''ApplicationArg
+
 patternVariables :: Pattern -> [VarName]
 patternVariables = \case
   PatternVariable v -> [v]
@@ -58,3 +68,189 @@ viewExpressionAsPattern e = case viewApp e of
     getVariable f = case f of
       ExpressionIden (IdenVar n) -> Just n
       _ -> Nothing
+
+addName :: Member (State (HashMap Name Name)) r => Name -> Name -> Sem r ()
+addName na nb = modify (HashMap.insert na nb)
+
+foldApplication :: Expression -> [ApplicationArg] -> Expression
+foldApplication f args = case args of
+  [] -> f
+  ((ApplicationArg i a) : as) -> foldApplication (ExpressionApplication (Application f a i)) as
+
+matchFunctionParameter ::
+  forall r.
+  Members '[State (HashMap Name Name), Reader (HashSet VarName), Error Text] r =>
+  FunctionParameter ->
+  FunctionParameter ->
+  Sem r ()
+matchFunctionParameter pa pb = do
+  goParamName (pa ^. paramName) (pb ^. paramName)
+  goParamUsage (pa ^. paramUsage) (pb ^. paramUsage)
+  goParamImplicit (pa ^. paramImplicit) (pb ^. paramImplicit)
+  goParamType (pa ^. paramType) (pb ^. paramType)
+  where
+    goParamType :: Expression -> Expression -> Sem r ()
+    goParamType ua ub = matchExpressions ua ub
+    goParamImplicit :: IsImplicit -> IsImplicit -> Sem r ()
+    goParamImplicit ua ub = unless (ua == ub) (throw @Text "implicit missmatch")
+    goParamUsage :: Usage -> Usage -> Sem r ()
+    goParamUsage ua ub = unless (ua == ub) (throw @Text "usage missmatch")
+    goParamName :: Maybe VarName -> Maybe VarName -> Sem r ()
+    goParamName (Just va) (Just vb) = addName va vb
+    goParamName _ _ = return ()
+
+matchExpressions ::
+  forall r.
+  Members '[State (HashMap Name Name), Reader (HashSet VarName), Error Text] r =>
+  Expression ->
+  Expression ->
+  Sem r ()
+matchExpressions = go
+  where
+    -- Soft free vars are allowed to be matched
+    isSoftFreeVar :: VarName -> Sem r Bool
+    isSoftFreeVar = asks . HashSet.member
+    go :: Expression -> Expression -> Sem r ()
+    go a b = case (a, b) of
+      (ExpressionIden ia, ExpressionIden ib) -> case (ia, ib) of
+        (IdenVar va, IdenVar vb) -> do
+          addIfFreeVar va vb
+          addIfFreeVar vb va
+          unlessM ((== Just vb) <$> gets @(HashMap Name Name) (^. at va)) err
+        (_, _) -> unless (ia == ib) err
+      (ExpressionIden {}, _) -> err
+      (_, ExpressionIden {}) -> err
+      (ExpressionApplication ia, ExpressionApplication ib) ->
+        goApp ia ib
+      (ExpressionApplication {}, _) -> err
+      (_, ExpressionApplication {}) -> err
+      (ExpressionUniverse ia, ExpressionUniverse ib) ->
+        unless (ia == ib) err
+      (ExpressionUniverse {}, _) -> err
+      (_, ExpressionUniverse {}) -> err
+      (ExpressionFunction ia, ExpressionFunction ib) ->
+        goFunction ia ib
+      (ExpressionFunction {}, _) -> err
+      (_, ExpressionFunction {}) -> err
+      (ExpressionLiteral ia, ExpressionLiteral ib) ->
+        unless (ia == ib) err
+      (ExpressionLiteral {}, _) -> err
+      (_, ExpressionLiteral {}) -> err
+      (ExpressionHole _, ExpressionHole _) -> return ()
+    addIfFreeVar :: VarName -> VarName -> Sem r ()
+    addIfFreeVar va vb = whenM (isSoftFreeVar va) (addName va vb)
+    err :: Sem r a
+    err = throw @Text "Expression missmatch"
+    goApp :: Application -> Application -> Sem r ()
+    goApp (Application al ar aim) (Application bl br bim) = do
+      unless (aim == bim) err
+      go al bl
+      go ar br
+    goFunction :: Function -> Function -> Sem r ()
+    goFunction (Function al ar) (Function bl br) = do
+      matchFunctionParameter al bl
+      matchExpressions ar br
+
+class IsExpression a where
+  toExpression :: a -> Expression
+
+instance IsExpression ConstructorRef where
+  toExpression = toExpression . IdenConstructor
+
+instance IsExpression InductiveRef where
+  toExpression = toExpression . IdenInductive
+
+instance IsExpression FunctionRef where
+  toExpression = toExpression . IdenFunction
+
+instance IsExpression AxiomRef where
+  toExpression = toExpression . IdenAxiom
+
+instance IsExpression Iden where
+  toExpression = ExpressionIden
+
+instance IsExpression Expression where
+  toExpression = id
+
+instance IsExpression Name where
+  toExpression n = case n ^. nameKind of
+    KNameConstructor -> toExpression (ConstructorRef n)
+    KNameInductive -> toExpression (InductiveRef n)
+    KNameFunction -> toExpression (FunctionRef n)
+    KNameAxiom -> toExpression (AxiomRef n)
+    KNameLocal -> toExpression (IdenVar n)
+    KNameLocalModule -> impossible
+    KNameTopModule -> impossible
+
+instance IsExpression Universe where
+  toExpression = ExpressionUniverse
+
+instance IsExpression Application where
+  toExpression = ExpressionApplication
+
+instance IsExpression Function where
+  toExpression = ExpressionFunction
+
+instance IsExpression ConstructorApp where
+  toExpression (ConstructorApp c args) =
+    foldApplication (toExpression c) (map toApplicationArg args)
+
+toApplicationArg :: Pattern -> ApplicationArg
+toApplicationArg = \case
+  PatternVariable v -> ApplicationArg Explicit (toExpression v)
+  PatternConstructorApp a -> ApplicationArg Explicit (toExpression a)
+  PatternEmpty -> impossible
+  PatternBraces p -> set appArgIsImplicit Implicit (toApplicationArg p)
+  PatternWildcard _ -> error "TODO"
+
+clauseLhsAsExpression :: FunctionClause -> Expression
+clauseLhsAsExpression cl =
+  foldApplication (toExpression (cl ^. clauseName)) (map toApplicationArg (cl ^. clausePatterns))
+
+infixr 0 -->
+
+(-->) :: (IsExpression a, IsExpression b) => a -> b -> Expression
+(-->) a b =
+  ExpressionFunction
+    ( Function
+        ( FunctionParameter
+            { _paramName = Nothing,
+              _paramUsage = UsageOmega,
+              _paramImplicit = Explicit,
+              _paramType = toExpression a
+            }
+        )
+        (toExpression b)
+    )
+
+infix 4 ===
+
+(===) :: (IsExpression a, IsExpression b) => a -> b -> Bool
+a === b = (toExpression a ==% toExpression b) mempty
+
+infix 4 ==%
+
+(==%) :: (IsExpression a, IsExpression b) => a -> b -> HashSet Name -> Bool
+(==%) a b free =
+  isRight
+    . run
+    . runError @Text
+    . runReader free
+    . evalState (mempty @(HashMap Name Name))
+    $ matchExpressions (toExpression a) (toExpression b)
+
+infixl 9 @@
+
+(@@) :: (IsExpression a, IsExpression b) => a -> b -> Expression
+a @@ b = toExpression (Application (toExpression a) (toExpression b) Explicit)
+
+freshVar :: Member NameIdGen r => Text -> Sem r VarName
+freshVar n = do
+  uid <- freshNameId
+  return
+    Name
+      { _nameId = uid,
+        _nameText = n,
+        _nameKind = KNameLocal,
+        _nameLoc = error "freshVar with no location"
+      }
diff --git a/src/MiniJuvix/Syntax/Abstract/Pretty.hs b/src/MiniJuvix/Syntax/Abstract/Pretty.hs
index fff09ed53a..511d157844 100644
--- a/src/MiniJuvix/Syntax/Abstract/Pretty.hs
+++ b/src/MiniJuvix/Syntax/Abstract/Pretty.hs
@@ -18,6 +18,9 @@ ppOutDefault = AnsiText . PPOutput . doc defaultOptions
 ppOut :: PrettyCode c => Options -> c -> AnsiText
 ppOut o = AnsiText . PPOutput . doc o
 
+ppSimple :: PrettyCode c => c -> Text
+ppSimple = toAnsiText True . ppOutDefault
+
 instance HasAnsiBackend PPOutput where
   toAnsiStream (PPOutput o) = reAnnotateS Ansi.stylize (layoutPretty defaultLayoutOptions o)
   toAnsiDoc (PPOutput o) = reAnnotate Ansi.stylize o
diff --git a/src/MiniJuvix/Syntax/Abstract/Pretty/Base.hs b/src/MiniJuvix/Syntax/Abstract/Pretty/Base.hs
index df84369afc..e3d7428631 100644
--- a/src/MiniJuvix/Syntax/Abstract/Pretty/Base.hs
+++ b/src/MiniJuvix/Syntax/Abstract/Pretty/Base.hs
@@ -11,8 +11,6 @@ import MiniJuvix.Syntax.Abstract.Language.Extra
 import MiniJuvix.Syntax.Abstract.Pretty.Ann
 import MiniJuvix.Syntax.Abstract.Pretty.Options
 import MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base qualified as S
-import MiniJuvix.Syntax.Universe
-import MiniJuvix.Syntax.Usage
 import Prettyprinter
 
 doc :: PrettyCode c => Options -> c -> Doc Ann
@@ -165,9 +163,10 @@ instance PrettyCode Name where
       if
           | showNameId -> Just . ("@" <>) <$> ppCode (n ^. nameId)
           | otherwise -> return Nothing
-    return $
-      annotate (AnnKind (n ^. nameKind)) $
-        pretty (n ^. nameText) <?> uid
+    return
+      $ annotate (AnnKind (n ^. nameKind))
+      $ pretty (n ^. nameText)
+      <?> uid
 
 instance PrettyCode Function where
   ppCode Function {..} = do
diff --git a/src/MiniJuvix/Syntax/Abstract/Quasiquoter.hs b/src/MiniJuvix/Syntax/Abstract/Quasiquoter.hs
new file mode 100644
index 0000000000..2b484e9ac5
--- /dev/null
+++ b/src/MiniJuvix/Syntax/Abstract/Quasiquoter.hs
@@ -0,0 +1,81 @@
+module MiniJuvix.Syntax.Abstract.Quasiquoter where
+
+--   ( module MiniJuvix.Syntax.Abstract.Quasiquoter,
+--     module MiniJuvix.Syntax.Abstract.Language,
+--   )
+-- where
+
+-- import Data.HashMap.Strict qualified as HashMap
+-- import Language.Haskell.TH (Exp, Q)
+-- import Language.Haskell.TH.Quote (QuasiQuoter (..))
+-- import Language.Haskell.TH.Syntax qualified as TH
+-- import MiniJuvix.Internal.NameIdGen (runNameIdGen)
+-- import MiniJuvix.Pipeline
+-- import MiniJuvix.Prelude
+-- import MiniJuvix.Syntax.Abstract.AbstractResult
+-- import MiniJuvix.Syntax.Abstract.Language
+
+-- minijuvixQ :: Lift a => (Module -> a) -> QuasiQuoter
+-- minijuvixQ proj =
+--   QuasiQuoter
+--     { quotePat = impossible,
+--       quoteType = impossible,
+--       quoteDec = impossible,
+--       quoteExp = minijuvixModule proj "Tmp" . wrapTmpModule
+--     }
+--     where
+--     wrapTmpModule :: String -> String
+--     wrapTmpModule body = "module Tmp;" <> body <> "end;"
+
+-- functionQ :: QuasiQuoter
+-- functionQ = minijuvixQ (getInd . getStatement)
+--   where
+--     getInd :: Statement -> FunctionDef
+--     getInd = \case
+--       StatementFunction d -> d
+--       _ -> error "function definition not found"
+
+-- inductiveQ :: QuasiQuoter
+-- inductiveQ = minijuvixQ (getInd . getStatement)
+--   where
+--     getInd :: Statement -> InductiveDef
+--     getInd = \case
+--       StatementInductive d -> d
+--       _ -> error "inductive definition not found"
+
+-- foreignQ :: QuasiQuoter
+-- foreignQ = minijuvixQ (getForeign . getStatement)
+--   where
+--     getForeign :: Statement -> ForeignBlock
+--     getForeign = \case
+--       StatementForeign d -> d
+--       _ -> error "foreign block not found"
+
+-- getStatement :: Module -> Statement
+-- getStatement = (^?! moduleBody . moduleStatements . _nonEmpty . _Just . _head)
+
+-- readAbsractModule :: String -> Text -> Either MiniJuvixError Module
+-- readAbsractModule name body =
+--   fmap (head . (^. resultModules))
+--     . run
+--     . runError
+--     . runNameIdGen
+--     . runFilesPure fs
+--     $ upToAbstract entry
+--   where
+--     fs :: HashMap FilePath Text
+--     fs = HashMap.singleton fakePath body
+--     entry :: EntryPoint
+--     entry =
+--       EntryPoint
+--         { _entryPointRoot = ".",
+--           _entryPointNoTermination = False,
+--           _entryPointModulePaths = fakePath :| []
+--         }
+--     fakePath :: FilePath
+--     fakePath = name <> ".mjuvix"
+
+-- minijuvixModule :: Lift a => (Module -> a) -> String -> String -> Q Exp
+-- minijuvixModule proj modName str = case readAbsractModule modName (pack str) of
+--   Left e -> fail ("Error: " <> unpack (renderText e))
+--   Right r -> TH.lift (proj r)
diff --git a/src/MiniJuvix/Syntax/Concrete/Builtins.hs b/src/MiniJuvix/Syntax/Concrete/Builtins.hs
new file mode 100644
index 0000000000..8dad41973c
--- /dev/null
+++ b/src/MiniJuvix/Syntax/Concrete/Builtins.hs
@@ -0,0 +1,81 @@
+module MiniJuvix.Syntax.Concrete.Builtins where
+
+import MiniJuvix.Internal.Strings qualified as Str
+import MiniJuvix.Prelude
+import MiniJuvix.Prelude.Pretty
+
+class IsBuiltin a where
+  toBuiltinPrim :: a -> BuiltinPrim
+
+instance IsBuiltin BuiltinInductive where
+  toBuiltinPrim = BuiltinsInductive
+
+instance IsBuiltin BuiltinConstructor where
+  toBuiltinPrim = BuiltinsConstructor
+
+instance IsBuiltin BuiltinFunction where
+  toBuiltinPrim = BuiltinsFunction
+
+instance IsBuiltin BuiltinAxiom where
+  toBuiltinPrim = BuiltinsAxiom
+
+data BuiltinPrim
+  = BuiltinsInductive BuiltinInductive
+  | BuiltinsConstructor BuiltinConstructor
+  | BuiltinsFunction BuiltinFunction
+  | BuiltinsAxiom BuiltinAxiom
+  deriving stock (Show, Eq, Ord, Generic)
+
+instance Hashable BuiltinPrim
+
+instance Pretty BuiltinPrim where
+  pretty = \case
+    BuiltinsInductive i -> pretty i
+    BuiltinsConstructor {} -> impossible
+    BuiltinsFunction f -> pretty f
+    BuiltinsAxiom a -> pretty a
+
+builtinConstructors :: BuiltinInductive -> [BuiltinConstructor]
+builtinConstructors = \case
+  BuiltinNatural -> [BuiltinNaturalZero, BuiltinNaturalSuc]
+
+data BuiltinInductive
+  = BuiltinNatural
+  deriving stock (Show, Eq, Ord, Enum, Bounded, Generic)
+
+instance Hashable BuiltinInductive
+
+instance Pretty BuiltinInductive where
+  pretty = \case
+    BuiltinNatural -> Str.natural
+
+data BuiltinConstructor
+  = BuiltinNaturalZero
+  | BuiltinNaturalSuc
+  deriving stock (Show, Eq, Ord, Generic)
+
+instance Hashable BuiltinConstructor
+
+data BuiltinFunction
+  = BuiltinNaturalPlus
+  deriving stock (Show, Eq, Ord, Enum, Bounded, Generic)
+
+instance Hashable BuiltinFunction
+
+instance Pretty BuiltinFunction where
+  pretty = \case
+    BuiltinNaturalPlus -> Str.naturalPlus
+
+data BuiltinAxiom
+  = BuiltinNaturalPrint
+  | BuiltinIO
+  | BuiltinIOSequence
+  deriving stock (Show, Eq, Ord, Enum, Bounded, Generic)
+
+instance Hashable BuiltinAxiom
+
+instance Pretty BuiltinAxiom where
+  pretty = \case
+    BuiltinNaturalPrint -> Str.naturalPrint
+    BuiltinIO -> Str.io
+    BuiltinIOSequence -> Str.ioSequence
diff --git a/src/MiniJuvix/Syntax/Concrete/Language.hs b/src/MiniJuvix/Syntax/Concrete/Language.hs
index ed802bd08a..333aa5c209 100644
--- a/src/MiniJuvix/Syntax/Concrete/Language.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Language.hs
@@ -4,6 +4,7 @@ module MiniJuvix.Syntax.Concrete.Language
   ( module MiniJuvix.Syntax.Concrete.Language,
     module MiniJuvix.Syntax.Concrete.Name,
     module MiniJuvix.Syntax.Concrete.Scoped.NameRef,
+    module MiniJuvix.Syntax.Concrete.Builtins,
     module MiniJuvix.Syntax.Concrete.Loc,
     module MiniJuvix.Syntax.Hole,
     module MiniJuvix.Syntax.Concrete.LiteralLoc,
@@ -24,6 +25,7 @@ where
 import Data.Kind qualified as GHC
 import MiniJuvix.Prelude hiding (show)
 import MiniJuvix.Syntax.Backends
+import MiniJuvix.Syntax.Concrete.Builtins
 import MiniJuvix.Syntax.Concrete.Language.Stage
 import MiniJuvix.Syntax.Concrete.LiteralLoc
 import MiniJuvix.Syntax.Concrete.Loc
@@ -182,6 +184,7 @@ instance HasLoc OperatorSyntaxDef where
 data TypeSignature (s :: Stage) = TypeSignature
   { _sigName :: FunctionName s,
     _sigType :: ExpressionType s,
+    _sigBuiltin :: Maybe BuiltinFunction,
     _sigTerminating :: Bool
   }
 
@@ -197,6 +200,7 @@ deriving stock instance (Ord (ExpressionType s), Ord (SymbolType s)) => Ord (Typ
 
 data AxiomDef (s :: Stage) = AxiomDef
   { _axiomName :: SymbolType s,
+    _axiomBuiltin :: Maybe BuiltinAxiom,
     _axiomType :: ExpressionType s
   }
 
@@ -237,7 +241,8 @@ deriving stock instance (Eq (ExpressionType s), Eq (SymbolType s)) => Eq (Induct
 deriving stock instance (Ord (ExpressionType s), Ord (SymbolType s)) => Ord (InductiveParameter s)
 
 data InductiveDef (s :: Stage) = InductiveDef
-  { _inductiveName :: InductiveName s,
+  { _inductiveBuiltin :: Maybe BuiltinInductive,
+    _inductiveName :: InductiveName s,
     _inductiveParameters :: [InductiveParameter s],
     _inductiveType :: Maybe (ExpressionType s),
     _inductiveConstructors :: [InductiveConstructorDef s]
diff --git a/src/MiniJuvix/Syntax/Concrete/Lexer.hs b/src/MiniJuvix/Syntax/Concrete/Lexer.hs
index 5741d98257..4e46c39455 100644
--- a/src/MiniJuvix/Syntax/Concrete/Lexer.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Lexer.hs
@@ -141,6 +141,7 @@ allKeywords :: Members '[Reader ParserParams, InfoTableBuilder] r => [ParsecS r
 allKeywords =
   [ kwAssignment,
     kwAxiom,
+    -- kwBuiltin, -- no need to be a reserved keyword
     kwColon,
     kwColonOmega,
     kwColonOne,
@@ -192,6 +193,9 @@ parens = between lparen rparen
 braces :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r a -> ParsecS r a
 braces = between (symbol "{") (symbol "}")
 
+kwBuiltin :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r ()
+kwBuiltin = keyword Str.builtin
+
 kwAssignment :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r ()
 kwAssignment = keyword Str.assignUnicode <|> keyword Str.assignAscii
 
diff --git a/src/MiniJuvix/Syntax/Concrete/Loc.hs b/src/MiniJuvix/Syntax/Concrete/Loc.hs
index 0d85171e3f..1682fc8467 100644
--- a/src/MiniJuvix/Syntax/Concrete/Loc.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Loc.hs
@@ -131,7 +131,8 @@ instance Pretty Loc where
 instance Pretty Interval where
   pretty :: Interval -> Doc a
   pretty i =
-    pretty (i ^. intervalFile) <> colon
+    pretty (i ^. intervalFile)
+      <> colon
       <> ppPosRange (i ^. intervalStart . locLine, i ^. intervalEnd . locLine)
       <> colon
       <> ppPosRange (i ^. intervalStart . locCol, i ^. intervalEnd . locCol)
diff --git a/src/MiniJuvix/Syntax/Concrete/Parser.hs b/src/MiniJuvix/Syntax/Concrete/Parser.hs
index bd0a1acba9..c308425688 100644
--- a/src/MiniJuvix/Syntax/Concrete/Parser.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Parser.hs
@@ -10,6 +10,7 @@ import Data.List.NonEmpty.Extra qualified as NonEmpty
 import Data.Singletons
 import MiniJuvix.Pipeline.EntryPoint
 import MiniJuvix.Prelude
+import MiniJuvix.Prelude.Pretty (Pretty, prettyText)
 import MiniJuvix.Syntax.Concrete.Base qualified as P
 import MiniJuvix.Syntax.Concrete.Language
 import MiniJuvix.Syntax.Concrete.Lexer hiding (symbol)
@@ -54,10 +55,21 @@ runModuleParser root fileName input =
         { _parserParamsRoot = root
         }
 
+top ::
+  Members '[Reader ParserParams, InfoTableBuilder] r =>
+  ParsecS r a ->
+  ParsecS r a
+top p = space >> p <* (optional kwSemicolon >> P.eof)
+
 topModuleDef ::
   Members '[Reader ParserParams, InfoTableBuilder] r =>
   ParsecS r (Module 'Parsed 'ModuleTop)
-topModuleDef = space >> moduleDef <* (optional kwSemicolon >> P.eof)
+topModuleDef = top moduleDef
+
+topStatement ::
+  Members '[Reader ParserParams, InfoTableBuilder] r =>
+  ParsecS r (Statement 'Parsed)
+topStatement = top statement
 
 --------------------------------------------------------------------------------
 -- Symbols and names
@@ -95,16 +107,59 @@ statement =
     <|> (StatementOpenModule <$> openModule)
     <|> (StatementEval <$> eval)
     <|> (StatementImport <$> import_)
-    <|> (StatementInductive <$> inductiveDef)
+    <|> (StatementInductive <$> inductiveDef Nothing)
     <|> (StatementPrint <$> printS)
     <|> (StatementForeign <$> foreignBlock)
     <|> (StatementModule <$> moduleDef)
-    <|> (StatementAxiom <$> axiomDef)
+    <|> (StatementAxiom <$> axiomDef Nothing)
     <|> (StatementCompile <$> compileBlock)
+    <|> builtinStatement
     <|> ( either StatementTypeSignature StatementFunctionClause
             <$> auxTypeSigFunClause
         )
 
+builtinInductive :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r BuiltinInductive
+builtinInductive = builtinHelper
+
+builtinFunction :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r BuiltinFunction
+builtinFunction = builtinHelper
+
+builtinAxiom :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r BuiltinAxiom
+builtinAxiom = builtinHelper
+
+builtinHelper ::
+  (Members '[Reader ParserParams, InfoTableBuilder] r, Bounded a, Enum a, Pretty a) =>
+  ParsecS r a
+builtinHelper =
+  P.choice
+    [ keyword (prettyText a) $> a
+      | a <- allElements
+    ]
+
+builtinInductiveDef :: Members '[Reader ParserParams, InfoTableBuilder] r => BuiltinInductive -> ParsecS r (InductiveDef 'Parsed)
+builtinInductiveDef = inductiveDef . Just
+
+builtinAxiomDef ::
+  Members '[Reader ParserParams, InfoTableBuilder] r =>
+  BuiltinAxiom ->
+  ParsecS r (AxiomDef 'Parsed)
+builtinAxiomDef = axiomDef . Just
+
+builtinTypeSig ::
+  Members '[Reader ParserParams, InfoTableBuilder] r =>
+  BuiltinFunction ->
+  ParsecS r (TypeSignature 'Parsed)
+builtinTypeSig b = do
+  fun <- symbol
+  typeSignature False fun (Just b)
+
+builtinStatement :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r (Statement 'Parsed)
+builtinStatement = do
+  kwBuiltin
+  (builtinInductive >>= fmap StatementInductive . builtinInductiveDef)
+    <|> (builtinFunction >>= fmap StatementTypeSignature . builtinTypeSig)
+    <|> (builtinAxiom >>= fmap StatementAxiom . builtinAxiomDef)
+
 --------------------------------------------------------------------------------
 -- Compile
 --------------------------------------------------------------------------------
@@ -275,16 +330,13 @@ typeSignature ::
   Members '[Reader ParserParams, InfoTableBuilder] r =>
   Bool ->
   Symbol ->
+  Maybe BuiltinFunction ->
   ParsecS r (TypeSignature 'Parsed)
-typeSignature _sigTerminating _sigName = do
+typeSignature _sigTerminating _sigName _sigBuiltin = do
   kwColon
   _sigType <- parseExpressionAtoms
   return TypeSignature {..}
 
--------------------------------------------------------------------------------
--- Aux type signature function clause
--------------------------------------------------------------------------------
-
 -- | Used to minimize the amount of required @P.try@s.
 auxTypeSigFunClause ::
   Members '[Reader ParserParams, InfoTableBuilder] r =>
@@ -292,15 +344,18 @@ auxTypeSigFunClause ::
 auxTypeSigFunClause = do
   terminating <- isJust <$> optional kwTerminating
   sym <- symbol
-  (Left <$> typeSignature terminating sym)
+  (Left <$> typeSignature terminating sym Nothing)
     <|> (Right <$> functionClause sym)
 
 -------------------------------------------------------------------------------
 -- Axioms
 -------------------------------------------------------------------------------
 
-axiomDef :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r (AxiomDef 'Parsed)
-axiomDef = do
+axiomDef ::
+  Members '[Reader ParserParams, InfoTableBuilder] r =>
+  Maybe BuiltinAxiom ->
+  ParsecS r (AxiomDef 'Parsed)
+axiomDef _axiomBuiltin = do
   kwAxiom
   _axiomName <- symbol
   kwColon
@@ -388,8 +443,8 @@ lambda = do
 -- Data type construction declaration
 -------------------------------------------------------------------------------
 
-inductiveDef :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r (InductiveDef 'Parsed)
-inductiveDef = do
+inductiveDef :: Members '[Reader ParserParams, InfoTableBuilder] r => Maybe BuiltinInductive -> ParsecS r (InductiveDef 'Parsed)
+inductiveDef _inductiveBuiltin = do
   kwInductive
   _inductiveName <- symbol
   _inductiveParameters <- P.many inductiveParam
diff --git a/src/MiniJuvix/Syntax/Concrete/Parser/InfoTableBuilder.hs b/src/MiniJuvix/Syntax/Concrete/Parser/InfoTableBuilder.hs
index 05f3ad1e5f..4dadd1a54c 100644
--- a/src/MiniJuvix/Syntax/Concrete/Parser/InfoTableBuilder.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Parser/InfoTableBuilder.hs
@@ -5,6 +5,7 @@ module MiniJuvix.Syntax.Concrete.Parser.InfoTableBuilder
     registerComment,
     mergeTable,
     runInfoTableBuilder,
+    ignoreInfoTableBuilder,
     module MiniJuvix.Syntax.Concrete.Parser.InfoTable,
   )
 where
@@ -68,7 +69,8 @@ build st = InfoTable (nubHashable (st ^. stateItems))
 
 runInfoTableBuilder :: Sem (InfoTableBuilder ': r) a -> Sem r (InfoTable, a)
 runInfoTableBuilder =
-  fmap (first build) . runState iniState
+  fmap (first build)
+    . runState iniState
     . reinterpret
       ( \case
           RegisterItem i ->
@@ -76,3 +78,6 @@ runInfoTableBuilder =
           MergeTable tbl ->
             modify' (over stateItems ((tbl ^. infoParsedItems) <>))
       )
+
+ignoreInfoTableBuilder :: Sem (InfoTableBuilder ': r) a -> Sem r a
+ignoreInfoTableBuilder = fmap snd . runInfoTableBuilder
diff --git a/src/MiniJuvix/Syntax/Concrete/Scoped/Error/Types.hs b/src/MiniJuvix/Syntax/Concrete/Scoped/Error/Types.hs
index e82e2a852b..adc817bdac 100644
--- a/src/MiniJuvix/Syntax/Concrete/Scoped/Error/Types.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Error/Types.hs
@@ -36,8 +36,11 @@ instance ToGenericError MultipleDeclarations where
       i1 :: Interval
       i1 = entryName _multipleDeclEntry ^. S.nameDefined
       msg =
-        "Multiple declarations of" <+> ppSymbolT _multipleDeclSymbol <> line
-          <> "Declared at:" <+> align (vsep lst)
+        "Multiple declarations of"
+          <+> ppSymbolT _multipleDeclSymbol
+            <> line
+            <> "Declared at:"
+          <+> align (vsep lst)
       lst = map pretty [L.symbolEntryToSName _multipleDeclEntry ^. S.nameDefined, _multipleDeclSecond]
 
 -- | megaparsec error while resolving infixities.
@@ -139,7 +142,8 @@ instance ToGenericError ImportCycle where
       h = head _importCycleImports
       i = getLoc h
       msg =
-        "There is an import cycle:" <> line
+        "There is an import cycle:"
+          <> line
           <> indent' (vsep (intersperse "⇓" (map pp (toList (tie _importCycleImports)))))
 
       pp :: Import 'Parsed -> Doc Eann
@@ -182,10 +186,11 @@ instance ToGenericError BindGroupConflict where
       i2 = getLoc _bindGroupSecond
 
       msg =
-        "The variable" <+> highlight (ppCode _bindGroupFirst)
+        "The variable"
+          <+> highlight (ppCode _bindGroupFirst)
           <+> "appears twice in the same binding group:"
-          <> line
-          <> indent' (align (vsep (map pretty [i1, i2])))
+            <> line
+            <> indent' (align (vsep (map pretty [i1, i2])))
 
 data DuplicateFixity = DuplicateFixity
   { _dupFixityFirst :: OperatorSyntaxDef,
@@ -207,9 +212,9 @@ instance ToGenericError DuplicateFixity where
       msg =
         "Multiple fixity declarations for symbol"
           <+> highlight (ppCode sym)
-          <> ":"
-          <> line
-          <> indent' (align locs)
+            <> ":"
+            <> line
+            <> indent' (align locs)
         where
           sym = _dupFixityFirst ^. opSymbol
           locs = vsep $ map (pretty . getLoc) [_dupFixityFirst, _dupFixityFirst]
@@ -231,7 +236,8 @@ instance ToGenericError MultipleExportConflict where
     where
       i = getLoc _multipleExportModule
       msg =
-        "The symbol" <+> highlight (ppCode _multipleExportSymbol)
+        "The symbol"
+          <+> highlight (ppCode _multipleExportSymbol)
           <+> "is exported multiple times in the module"
           <+> ppCode _multipleExportModule
 
@@ -294,9 +300,11 @@ instance ToGenericError AppLeftImplicit where
     where
       i = getLoc (e ^. appLeftImplicit)
       msg =
-        "The expression" <+> ppCode (e ^. appLeftImplicit) <+> "cannot appear by itself."
-          <> line
-          <> "It needs to be the argument of a function expecting an implicit argument."
+        "The expression"
+          <+> ppCode (e ^. appLeftImplicit)
+          <+> "cannot appear by itself."
+            <> line
+            <> "It needs to be the argument of a function expecting an implicit argument."
 
 newtype ModuleNotInScope = ModuleNotInScope
   { _moduleNotInScopeName :: Name
@@ -339,7 +347,8 @@ instance ToGenericError UnusedOperatorDef where
     where
       i = getLoc _unusedOperatorDef
       msg =
-        "Unused operator syntax definition:" <> line
+        "Unused operator syntax definition:"
+          <> line
           <> ppCode _unusedOperatorDef
 
 data WrongTopModuleName = WrongTopModuleName
@@ -359,14 +368,15 @@ instance ToGenericError WrongTopModuleName where
     where
       i = getLoc _wrongTopModuleNameActualName
       msg =
-        "The top module" <+> ppCode _wrongTopModuleNameActualName
+        "The top module"
+          <+> ppCode _wrongTopModuleNameActualName
           <+> "is defined in the file:"
-          <> line
-          <> highlight (pretty _wrongTopModuleNameActualPath)
-          <> line
-          <> "But it should be in the file:"
-          <> line
-          <> pretty _wrongTopModuleNameExpectedPath
+            <> line
+            <> highlight (pretty _wrongTopModuleNameActualPath)
+            <> line
+            <> "But it should be in the file:"
+            <> line
+            <> pretty _wrongTopModuleNameExpectedPath
 
 data AmbiguousSym = AmbiguousSym
   { _ambiguousSymName :: Name,
@@ -421,10 +431,11 @@ instance ToGenericError WrongLocationCompileBlock where
       name = _wrongLocationCompileBlockName
       i = getLoc name
       msg =
-        "The compilation rules for the symbol" <+> highlight (ppCode name)
+        "The compilation rules for the symbol"
+          <+> highlight (ppCode name)
           <+> "need to be defined in the module:"
-          <> line
-          <> highlight (ppCode _wrongLocationCompileBlockExpectedModPath)
+            <> line
+            <> highlight (ppCode _wrongLocationCompileBlockExpectedModPath)
 
 data MultipleCompileBlockSameName = MultipleCompileBlockSameName
   { _multipleCompileBlockFirstDefined :: Interval,
@@ -464,7 +475,8 @@ instance ToGenericError MultipleCompileRuleSameBackend where
       name = _multipleCompileRuleSameBackendSym
       i = getLoc _multipleCompileRuleSameBackendSym
       msg =
-        "Multiple" <+> highlight (ppCode backend)
+        "Multiple"
+          <+> highlight (ppCode backend)
           <+> "compilation rules for the symbol"
           <+> highlight (ppCode name)
           <+> "at"
@@ -486,18 +498,27 @@ instance ToGenericError WrongKindExpressionCompileBlock where
     where
       i = getLoc _wrongKindExpressionCompileBlockSym
       msg =
-        "Symbol" <+> ppCode _wrongKindExpressionCompileBlockSym
+        "Symbol"
+          <+> ppCode _wrongKindExpressionCompileBlockSym
           <+> "is not a constructor, inductive data type, axiom nor a function."
-          <> "Thus, it cannot have a compile rule."
+            <> "Thus, it cannot have a compile rule."
 
 infixErrorAux :: Doc Eann -> Doc Eann -> Doc Eann
 infixErrorAux kind pp =
-  "Error while resolving infixities in the" <+> kind <> ":" <> line
-    <> indent' (highlight pp)
+  "Error while resolving infixities in the"
+    <+> kind
+      <> ":"
+      <> line
+      <> indent' (highlight pp)
 
 ambiguousMessage :: Name -> [SymbolEntry] -> Doc Eann
 ambiguousMessage n es =
-  "The symbol" <+> ppCode n <+> "at" <+> pretty (getLoc n) <+> "is ambiguous." <> line
-    <> "It could be any of:"
-    <> line
-    <> indent' (vsep (map ppCode es))
+  "The symbol"
+    <+> ppCode n
+    <+> "at"
+    <+> pretty (getLoc n)
+    <+> "is ambiguous."
+      <> line
+      <> "It could be any of:"
+      <> line
+      <> indent' (vsep (map ppCode es))
diff --git a/src/MiniJuvix/Syntax/Concrete/Scoped/Name/NameKind.hs b/src/MiniJuvix/Syntax/Concrete/Scoped/Name/NameKind.hs
index 769880c856..c42d766a25 100644
--- a/src/MiniJuvix/Syntax/Concrete/Scoped/Name/NameKind.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Name/NameKind.hs
@@ -1,6 +1,7 @@
 module MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind where
 
 import MiniJuvix.Prelude
+import MiniJuvix.Prelude.Pretty
 import Prettyprinter.Render.Terminal
 
 data NameKind
@@ -26,6 +27,16 @@ class HasNameKind a where
 instance HasNameKind NameKind where
   getNameKind = id
 
+instance Pretty NameKind where
+  pretty = \case
+    KNameConstructor -> "constructor"
+    KNameInductive -> "inductive type"
+    KNameFunction -> "function"
+    KNameLocal -> "variable"
+    KNameAxiom -> "axiom"
+    KNameLocalModule -> "local module"
+    KNameTopModule -> "module"
+
 isLocallyBounded :: HasNameKind a => a -> Bool
 isLocallyBounded k = case getNameKind k of
   KNameLocal -> True
diff --git a/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Base.hs b/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Base.hs
index 8be05d4dd2..99ea51d596 100644
--- a/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Base.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Base.hs
@@ -28,8 +28,11 @@ class PrettyCode a where
 runPrettyCode :: PrettyCode c => Options -> c -> Doc Ann
 runPrettyCode opts = run . runReader opts . ppCode
 
+keyword' :: Pretty a => a -> Doc Ann
+keyword' = annotate AnnKeyword . pretty
+
 keyword :: Text -> Doc Ann
-keyword = annotate AnnKeyword . pretty
+keyword = keyword'
 
 delimiter :: Text -> Doc Ann
 delimiter = annotate AnnDelimiter . pretty
@@ -40,6 +43,12 @@ kwModule = keyword Str.module_
 kwEnd :: Doc Ann
 kwEnd = keyword Str.end
 
+kwBuiltin :: Doc Ann
+kwBuiltin = keyword Str.builtin
+
+kwNatural :: Doc Ann
+kwNatural = keyword Str.natural
+
 kwInductive :: Doc Ann
 kwInductive = keyword Str.inductive
 
@@ -221,15 +230,19 @@ groupStatements = reverse . map reverse . uncurry cons . foldl' aux ([], [])
     g :: Statement s -> Statement s -> Bool
     g a b = case (a, b) of
       (StatementForeign _, _) -> False
-      (StatementCompile _, _) -> False -- TODO: not sure
+      (StatementCompile _, _) -> False
       (StatementOperator _, StatementOperator _) -> True
       (StatementOperator o, s) -> definesSymbol (o ^. opSymbol) s
       (StatementImport _, StatementImport _) -> True
       (StatementImport i, StatementOpenModule o) -> case sing :: SStage s of
         SParsed -> True
         SScoped ->
-          i ^. importModule . modulePath . S.nameId
-            == projSigma2 (^. moduleRefName) (o ^. openModuleName . unModuleRef') ^. S.nameId
+          i
+            ^. importModule
+            . modulePath
+            . S.nameId
+            == projSigma2 (^. moduleRefName) (o ^. openModuleName . unModuleRef')
+            ^. S.nameId
       (StatementImport _, _) -> False
       (StatementOpenModule {}, StatementOpenModule {}) -> True
       (StatementOpenModule {}, _) -> False
@@ -253,20 +266,22 @@ groupStatements = reverse . map reverse . uncurry cons . foldl' aux ([], [])
       (StatementFunctionClause {}, _) -> False
     definesSymbol :: Symbol -> Statement s -> Bool
     definesSymbol n s = case s of
-      StatementTypeSignature sig ->
-        let sym = case sing :: SStage s of
-              SParsed -> sig ^. sigName
-              SScoped -> sig ^. sigName . S.nameConcrete
-         in n == sym
+      StatementTypeSignature sig -> n == symbolParsed (sig ^. sigName)
       StatementInductive d -> n `elem` syms d
+      StatementAxiom d -> n == symbolParsed (d ^. axiomName)
       _ -> False
       where
+        symbolParsed :: SymbolType s -> Symbol
+        symbolParsed sym = case sing :: SStage s of
+          SParsed -> sym
+          SScoped -> sym ^. S.nameConcrete
         syms :: InductiveDef s -> [Symbol]
         syms InductiveDef {..} = case sing :: SStage s of
           SParsed -> _inductiveName : map (^. constructorName) _inductiveConstructors
           SScoped ->
-            _inductiveName ^. S.nameConcrete :
-            map (^. constructorName . S.nameConcrete) _inductiveConstructors
+            _inductiveName
+              ^. S.nameConcrete
+              : map (^. constructorName . S.nameConcrete) _inductiveConstructors
 
 instance SingI s => PrettyCode [Statement s] where
   ppCode ss = vsep2 <$> mapM (fmap vsep . mapM (fmap endSemicolon . ppCode)) (groupStatements ss)
@@ -301,10 +316,13 @@ instance PrettyCode ForeignBlock where
   ppCode ForeignBlock {..} = do
     _foreignBackend' <- ppCode _foreignBackend
     return $
-      kwForeign <+> _foreignBackend' <+> lbrace <> line
-        <> pretty (escape _foreignCode)
-        <> line
-        <> rbrace
+      kwForeign
+        <+> _foreignBackend'
+        <+> lbrace
+          <> line
+          <> pretty (escape _foreignCode)
+          <> line
+          <> rbrace
     where
       escape :: Text -> Text
       escape = T.replace "}" "\\}"
@@ -360,12 +378,16 @@ instance (SingI s, SingI t) => PrettyCode (Module s t) where
     moduleBody' <- ppCode _moduleBody >>= indented
     modulePath' <- ppModulePathType _modulePath
     moduleParameters' <- ppInductiveParameters _moduleParameters
-    return $
-      kwModule <+> modulePath' <+?> moduleParameters' <> kwSemicolon <> line
-        <> moduleBody'
-        <> line
-        <> kwEnd
-        <?> lastSemicolon
+    return
+      $ kwModule
+        <+> modulePath'
+        <+?> moduleParameters'
+          <> kwSemicolon
+          <> line
+          <> moduleBody'
+          <> line
+          <> kwEnd
+      <?> lastSemicolon
     where
       lastSemicolon = case sing :: SModuleIsTop t of
         SModuleLocal -> Nothing
@@ -403,6 +425,15 @@ instance SingI s => PrettyCode (InductiveConstructorDef s) where
     constructorType' <- ppExpression _constructorType
     return $ constructorName' <+> kwColon <+> constructorType'
 
+instance PrettyCode BuiltinInductive where
+  ppCode i = return (kwBuiltin <+> keyword' i)
+
+instance PrettyCode BuiltinFunction where
+  ppCode i = return (kwBuiltin <+> keyword' i)
+
+instance PrettyCode BuiltinAxiom where
+  ppCode i = return (kwBuiltin <+> keyword' i)
+
 instance SingI s => PrettyCode (InductiveDef s) where
   ppCode :: forall r. Members '[Reader Options] r => InductiveDef s -> Sem r (Doc Ann)
   ppCode InductiveDef {..} = do
@@ -410,8 +441,13 @@ instance SingI s => PrettyCode (InductiveDef s) where
     inductiveParameters' <- ppInductiveParameters _inductiveParameters
     inductiveType' <- ppTypeType
     inductiveConstructors' <- ppBlock _inductiveConstructors
+    inductivebuiltin' <- traverse ppCode _inductiveBuiltin
     return $
-      kwInductive <+> inductiveName' <+?> inductiveParameters' <+?> inductiveType'
+      inductivebuiltin'
+        <?+> kwInductive
+        <+> inductiveName'
+        <+?> inductiveParameters'
+        <+?> inductiveType'
         <+> inductiveConstructors'
     where
       ppTypeType :: Sem r (Maybe (Doc Ann))
@@ -515,7 +551,8 @@ instance SingI s => PrettyCode (TypeSignature s) where
     let sigTerminating' = if _sigTerminating then kwTerminating <> line else mempty
     sigName' <- annDef _sigName <$> ppSymbol _sigName
     sigType' <- ppExpression _sigType
-    return $ sigTerminating' <> sigName' <+> kwColon <+> sigType'
+    builtin' <- traverse ppCode _sigBuiltin
+    return $ builtin' <?+> sigTerminating' <> sigName' <+> kwColon <+> sigType'
 
 instance SingI s => PrettyCode (Function s) where
   ppCode :: forall r. Members '[Reader Options] r => Function s -> Sem r (Doc Ann)
@@ -597,7 +634,10 @@ instance SingI s => PrettyCode (FunctionClause s) where
     clauseBody' <- ppExpression _clauseBody
     clauseWhere' <- mapM ppCode _clauseWhere
     return $
-      clauseOwnerFunction' <+?> clausePatterns' <+> kwAssignment <+> clauseBody'
+      clauseOwnerFunction'
+        <+?> clausePatterns'
+        <+> kwAssignment
+        <+> clauseBody'
         <+?> ((line <>) <$> clauseWhere')
 
 instance SingI s => PrettyCode (WhereBlock s) where
@@ -613,7 +653,8 @@ instance SingI s => PrettyCode (AxiomDef s) where
   ppCode AxiomDef {..} = do
     axiomName' <- ppSymbol _axiomName
     axiomType' <- ppExpression _axiomType
-    return $ kwAxiom <+> axiomName' <+> kwColon <+> axiomType'
+    builtin' <- traverse ppCode _axiomBuiltin
+    return $ builtin' <?+> kwAxiom <+> axiomName' <+> kwColon <+> axiomType'
 
 instance SingI s => PrettyCode (Eval s) where
   ppCode (Eval p) = do
@@ -842,7 +883,8 @@ ppExpression = case sing :: SStage s of
 instance PrettyCode SymbolEntry where
   ppCode ent =
     return
-      ( kindTag <+> pretty (entryName ent ^. S.nameVerbatim)
+      ( kindTag
+          <+> pretty (entryName ent ^. S.nameVerbatim)
           <+> "defined at"
           <+> pretty (getLoc ent)
       )
diff --git a/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Html.hs b/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Html.hs
index 766a536baa..2d151906f5 100644
--- a/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Html.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Html.hs
@@ -75,7 +75,9 @@ genModule opts printMetadata utc theme m =
     prettySrc :: Html
     prettySrc =
       (pre ! Attr.id "src-content") $
-        renderTree $ treeForm $ docStream' opts m
+        renderTree $
+          treeForm $
+            docStream' opts m
 
     mheader :: Html
     mheader =
@@ -167,7 +169,8 @@ nameIdAttrRef tp s =
 
 cssLink :: AttributeValue -> Html
 cssLink css =
-  link ! Attr.href css
+  link
+    ! Attr.href css
     ! Attr.rel "stylesheet"
     ! Attr.type_ "text/css"
 
@@ -179,7 +182,8 @@ nordCss = cssLink "assets/source-nord.css"
 
 highlightJs :: Html
 highlightJs =
-  script ! Attr.src "assets/highlight.js"
+  script
+    ! Attr.src "assets/highlight.js"
     ! Attr.type_ "text/javascript"
     $ mempty
 
diff --git a/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper.hs b/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper.hs
index e1947eddee..ed92a25a97 100644
--- a/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper.hs
@@ -252,7 +252,10 @@ lookupSymbolAux modules final = do
             Nothing -> []
             Just SymbolInfo {..} -> toList _symbolInfo
         (p : ps) ->
-          mapMaybe (lookInExport final ps . getModuleExportInfo) . concat . maybeToList . fmap (mapMaybe getModuleRef . toList . (^. symbolInfo))
+          mapMaybe (lookInExport final ps . getModuleExportInfo)
+            . concat
+            . maybeToList
+            . fmap (mapMaybe getModuleRef . toList . (^. symbolInfo))
             . HashMap.lookup p
             <$> gets (^. scopeSymbols)
     importedTopModule :: Sem r (Maybe SymbolEntry)
@@ -458,6 +461,7 @@ checkInductiveDef InductiveDef {..} = do
     registerInductive'
       InductiveDef
         { _inductiveName = inductiveName',
+          _inductiveBuiltin = _inductiveBuiltin,
           _inductiveParameters = inductiveParameters',
           _inductiveType = inductiveType',
           _inductiveConstructors = inductiveConstructors'
diff --git a/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper/InfoTableBuilder.hs b/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper/InfoTableBuilder.hs
index 770adf0316..b31f9bc19c 100644
--- a/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper/InfoTableBuilder.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper/InfoTableBuilder.hs
@@ -93,3 +93,6 @@ toState = reinterpret $ \case
 
 runInfoTableBuilder :: Sem (InfoTableBuilder ': r) a -> Sem r (InfoTable, a)
 runInfoTableBuilder = runState emptyInfoTable . toState
+
+ignoreInfoTableBuilder :: Sem (InfoTableBuilder ': r) a -> Sem r a
+ignoreInfoTableBuilder = evalState emptyInfoTable . toState
diff --git a/src/MiniJuvix/Syntax/Fixity.hs b/src/MiniJuvix/Syntax/Fixity.hs
index 862e524c61..8637336bf0 100644
--- a/src/MiniJuvix/Syntax/Fixity.hs
+++ b/src/MiniJuvix/Syntax/Fixity.hs
@@ -1,13 +1,12 @@
 module MiniJuvix.Syntax.Fixity where
 
-import Language.Haskell.TH.Syntax (Lift)
 import MiniJuvix.Prelude
 
 data Precedence
   = PrecMinusOmega
   | PrecNat Natural
   | PrecOmega
-  deriving stock (Show, Eq, Lift)
+  deriving stock (Show, Eq)
 
 instance Ord Precedence where
   compare a b = case (a, b) of
@@ -20,21 +19,21 @@ instance Ord Precedence where
     (PrecOmega, _) -> GT
 
 data UnaryAssoc = AssocPostfix
-  deriving stock (Show, Eq, Ord, Lift)
+  deriving stock (Show, Eq, Ord)
 
 data BinaryAssoc = AssocNone | AssocLeft | AssocRight
-  deriving stock (Show, Eq, Ord, Lift)
+  deriving stock (Show, Eq, Ord)
 
 data OperatorArity
   = Unary UnaryAssoc
   | Binary BinaryAssoc
-  deriving stock (Show, Eq, Ord, Lift)
+  deriving stock (Show, Eq, Ord)
 
 data Fixity = Fixity
   { _fixityPrecedence :: Precedence,
     _fixityArity :: OperatorArity
   }
-  deriving stock (Show, Eq, Ord, Lift)
+  deriving stock (Show, Eq, Ord)
 
 makeLenses ''Fixity
 
diff --git a/src/MiniJuvix/Syntax/MicroJuvix/ArityChecker/Error/Types.hs b/src/MiniJuvix/Syntax/MicroJuvix/ArityChecker/Error/Types.hs
index 61ec88471f..40974fe816 100644
--- a/src/MiniJuvix/Syntax/MicroJuvix/ArityChecker/Error/Types.hs
+++ b/src/MiniJuvix/Syntax/MicroJuvix/ArityChecker/Error/Types.hs
@@ -27,7 +27,7 @@ instance ToGenericError WrongConstructorAppLength where
           <+> ppCode (e ^. wrongConstructorAppLength . constrAppConstructor)
           <+> "should have"
           <+> arguments (e ^. wrongConstructorAppLengthExpected)
-          <> ", but has been given"
+            <> ", but has been given"
           <+> pretty actual
 
       actual :: Int
@@ -105,13 +105,15 @@ instance ToGenericError ExpectedExplicitArgument where
       arg = snd (toList args !! idx)
       i = getLoc arg
       msg =
-        "Expected an explicit argument as the" <+> ordinal (succ idx) <+> "argument of"
+        "Expected an explicit argument as the"
+          <+> ordinal (succ idx)
+          <+> "argument of"
           <+> ppCode f
           <+> "but found"
           <+> ppArg Implicit arg
-          <> "."
-          <> softline
-          <> "In the application"
+            <> "."
+            <> softline
+            <> "In the application"
           <+> ppApp app
 
 newtype PatternFunction = PatternFunction
@@ -130,7 +132,8 @@ instance ToGenericError PatternFunction where
     where
       i = getLoc (e ^. patternFunction)
       msg =
-        "Invalid pattern" <+> ppCode (e ^. patternFunction) <> "."
+        "Invalid pattern"
+          <+> ppCode (e ^. patternFunction) <> "."
           <+> "Function types cannot be pattern matched"
 
 data TooManyArguments = TooManyArguments
@@ -158,12 +161,13 @@ instance ToGenericError TooManyArguments where
       app :: Expression
       app = foldApplication fun args
       msg =
-        "Too many arguments in the application" <+> ppCode app <> "."
+        "Too many arguments in the application"
+          <+> ppCode app <> "."
           <+> "The last"
           <+> numArguments
-          <> ", namely"
+            <> ", namely"
           <+> ppUnexpectedArgs
-          <> ","
+            <> ","
           <+> wasNotExpected
       numArguments :: Doc ann
       numArguments = plural "argument" (pretty numUnexpected <+> "arguments") numUnexpected
@@ -191,5 +195,7 @@ instance ToGenericError FunctionApplied where
       args = e ^. functionAppliedArguments
       fun = ExpressionFunction (e ^. functionAppliedFunction)
       msg =
-        "A function type cannot be applied." <> softline
-          <> "In the application" <+> ppApp (fun, args)
+        "A function type cannot be applied."
+          <> softline
+          <> "In the application"
+          <+> ppApp (fun, args)
diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Error/Types.hs b/src/MiniJuvix/Syntax/MicroJuvix/Error/Types.hs
index 55888b1f03..b0b681cdee 100644
--- a/src/MiniJuvix/Syntax/MicroJuvix/Error/Types.hs
+++ b/src/MiniJuvix/Syntax/MicroJuvix/Error/Types.hs
@@ -232,7 +232,7 @@ instance ToGenericError WrongNumberArgumentsIndType where
                     | expectedNumArgs == 1 -> "one argument"
                     | otherwise -> pretty expectedNumArgs <+> "arguments"
               )
-          <> ", but"
+            <> ", but"
           <+> ( if
                     | actualNumArgs == 0 -> "no argument is"
                     | actualNumArgs == 1 -> "only one argument is"
diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Language.hs b/src/MiniJuvix/Syntax/MicroJuvix/Language.hs
index d96932f7a4..0ca1d8e9ec 100644
--- a/src/MiniJuvix/Syntax/MicroJuvix/Language.hs
+++ b/src/MiniJuvix/Syntax/MicroJuvix/Language.hs
@@ -6,11 +6,13 @@ module MiniJuvix.Syntax.MicroJuvix.Language
     module MiniJuvix.Syntax.Hole,
     module MiniJuvix.Syntax.Wildcard,
     module MiniJuvix.Syntax.Concrete.LiteralLoc,
+    module MiniJuvix.Syntax.Concrete.Builtins,
   )
 where
 
 import MiniJuvix.Prelude
 import MiniJuvix.Syntax.Abstract.Name
+import MiniJuvix.Syntax.Concrete.Builtins
 import MiniJuvix.Syntax.Concrete.LiteralLoc
 import MiniJuvix.Syntax.Concrete.Loc
 import MiniJuvix.Syntax.ForeignBlock
@@ -40,13 +42,15 @@ data Statement
 
 data AxiomDef = AxiomDef
   { _axiomName :: AxiomName,
+    _axiomBuiltin :: Maybe BuiltinAxiom,
     _axiomType :: Type
   }
 
 data FunctionDef = FunctionDef
   { _funDefName :: FunctionName,
     _funDefType :: Type,
-    _funDefClauses :: NonEmpty FunctionClause
+    _funDefClauses :: NonEmpty FunctionClause,
+    _funDefBuiltin :: Maybe BuiltinFunction
   }
 
 data FunctionClause = FunctionClause
@@ -112,6 +116,7 @@ newtype InductiveParameter = InductiveParameter
 
 data InductiveDef = InductiveDef
   { _inductiveName :: InductiveName,
+    _inductiveBuiltin :: Maybe BuiltinInductive,
     _inductiveParameters :: [InductiveParameter],
     _inductiveConstructors :: [InductiveConstructorDef]
   }
diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Language/Extra.hs b/src/MiniJuvix/Syntax/MicroJuvix/Language/Extra.hs
index c60a57c152..c06a79e0ed 100644
--- a/src/MiniJuvix/Syntax/MicroJuvix/Language/Extra.hs
+++ b/src/MiniJuvix/Syntax/MicroJuvix/Language/Extra.hs
@@ -151,7 +151,8 @@ fillHolesFunctionDef m d =
   FunctionDef
     { _funDefName = d ^. funDefName,
       _funDefType = fillHolesType m (d ^. funDefType),
-      _funDefClauses = fmap (fillHolesClause m) (d ^. funDefClauses)
+      _funDefClauses = fmap (fillHolesClause m) (d ^. funDefClauses),
+      _funDefBuiltin = d ^. funDefBuiltin
     }
 
 fillHolesClause :: HashMap Hole Type -> FunctionClause -> FunctionClause
diff --git a/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Base.hs b/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Base.hs
index d2f1e71a09..ed3d1e98da 100644
--- a/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Base.hs
+++ b/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Base.hs
@@ -38,9 +38,10 @@ instance PrettyCode Name where
       if
           | showNameId -> Just . ("@" <>) <$> ppCode (n ^. nameId)
           | otherwise -> return Nothing
-    return $
-      annotate (AnnKind (n ^. nameKind)) $
-        pretty (n ^. nameText) <?> uid
+    return
+      $ annotate (AnnKind (n ^. nameKind))
+      $ pretty (n ^. nameText)
+      <?> uid
 
 instance PrettyCode Iden where
   ppCode :: Member (Reader Options) r => Iden -> Sem r (Doc Ann)
@@ -242,8 +243,11 @@ instance PrettyCode FunctionDef where
     funDefType' <- ppCode (f ^. funDefType)
     clauses' <- mapM ppCode (f ^. funDefClauses)
     return $
-      funDefName' <+> kwColonColon <+> funDefType' <> line
-        <> vsep (toList clauses')
+      funDefName'
+        <+> kwColonColon
+        <+> funDefType'
+          <> line
+          <> vsep (toList clauses')
 
 instance PrettyCode FunctionClause where
   ppCode c = do
@@ -261,10 +265,13 @@ instance PrettyCode ForeignBlock where
   ppCode ForeignBlock {..} = do
     _foreignBackend' <- ppCode _foreignBackend
     return $
-      kwForeign <+> _foreignBackend' <+> lbrace <> line
-        <> pretty _foreignCode
-        <> line
-        <> rbrace
+      kwForeign
+        <+> _foreignBackend'
+        <+> lbrace
+          <> line
+          <> pretty _foreignCode
+          <> line
+          <> rbrace
 
 instance PrettyCode Include where
   ppCode i = do
@@ -295,11 +302,13 @@ instance PrettyCode Module where
     name' <- ppCode (m ^. moduleName)
     body' <- ppCode (m ^. moduleBody)
     return $
-      kwModule <+> name' <+> kwWhere
-        <> line
-        <> line
-        <> body'
-        <> line
+      kwModule
+        <+> name'
+        <+> kwWhere
+          <> line
+          <> line
+          <> body'
+          <> line
 
 instance PrettyCode TypeCallIden where
   ppCode = \case
diff --git a/src/MiniJuvix/Syntax/MiniHaskell/Pretty/Base.hs b/src/MiniJuvix/Syntax/MiniHaskell/Pretty/Base.hs
index 1c2b9f4d16..dbd7836cae 100644
--- a/src/MiniJuvix/Syntax/MiniHaskell/Pretty/Base.hs
+++ b/src/MiniJuvix/Syntax/MiniHaskell/Pretty/Base.hs
@@ -122,8 +122,11 @@ instance PrettyCode FunctionDef where
     funDefTypeSig' <- ppCode (f ^. funDefType)
     clauses' <- mapM (ppClause funDefName') (f ^. funDefClauses)
     return $
-      funDefName' <+> kwColonColon <+> funDefTypeSig' <> line
-        <> vsep (toList clauses')
+      funDefName'
+        <+> kwColonColon
+        <+> funDefTypeSig'
+          <> line
+          <> vsep (toList clauses')
     where
       ppClause :: Member (Reader Options) r => Doc Ann -> FunctionClause -> Sem r (Doc Ann)
       ppClause fun c = do
@@ -164,11 +167,13 @@ instance PrettyCode Module where
     name' <- ppCode (m ^. moduleName)
     body' <- ppCode (m ^. moduleBody)
     return $
-      kwModule <+> name' <+> kwWhere
-        <> line
-        <> line
-        <> body'
-        <> line
+      kwModule
+        <+> name'
+        <+> kwWhere
+          <> line
+          <> line
+          <> body'
+          <> line
 
 parensCond :: Bool -> Doc Ann -> Doc Ann
 parensCond t d = if t then parens d else d
diff --git a/src/MiniJuvix/Syntax/MonoJuvix/InfoTable.hs b/src/MiniJuvix/Syntax/MonoJuvix/InfoTable.hs
index beb8cc2772..0165d628e8 100644
--- a/src/MiniJuvix/Syntax/MonoJuvix/InfoTable.hs
+++ b/src/MiniJuvix/Syntax/MonoJuvix/InfoTable.hs
@@ -6,20 +6,28 @@ import MiniJuvix.Syntax.MonoJuvix.Language
 
 data ConstructorInfo = ConstructorInfo
   { _constructorInfoArgs :: [Type],
-    _constructorInfoInductive :: InductiveName
+    _constructorInfoInductive :: InductiveName,
+    _constructorInfoBuiltin :: Maybe BuiltinConstructor
+  }
+
+newtype InductiveInfo = InductiveInfo
+  { _inductiveInfoBuiltin :: Maybe BuiltinInductive
   }
 
 data FunctionInfo = FunctionInfo
   { _functionInfoType :: Type,
-    _functionInfoPatterns :: Int
+    _functionInfoPatterns :: Int,
+    _functionInfoBuiltin :: Maybe BuiltinFunction
   }
 
-newtype AxiomInfo = AxiomInfo
-  { _axiomInfoType :: Type
+data AxiomInfo = AxiomInfo
+  { _axiomInfoType :: Type,
+    _axiomInfoBuiltin :: Maybe BuiltinAxiom
   }
 
 data InfoTable = InfoTable
-  { _infoConstructors :: HashMap Name ConstructorInfo,
+  { _infoInductives :: HashMap Name InductiveInfo,
+    _infoConstructors :: HashMap Name ConstructorInfo,
     _infoAxioms :: HashMap Name AxiomInfo,
     _infoFunctions :: HashMap Name FunctionInfo
   }
@@ -27,25 +35,50 @@ data InfoTable = InfoTable
 buildTable :: Module -> InfoTable
 buildTable m = InfoTable {..}
   where
+    _infoInductives :: HashMap Name InductiveInfo
+    _infoInductives =
+      HashMap.fromList
+        [ (d ^. inductiveName, InductiveInfo (d ^. inductiveBuiltin))
+          | StatementInductive d <- ss
+        ]
     _infoConstructors :: HashMap Name ConstructorInfo
     _infoConstructors =
       HashMap.fromList
-        [ (c ^. constructorName, ConstructorInfo args ind)
+        [ ( c ^. constructorName,
+            ConstructorInfo
+              { _constructorInfoArgs = args,
+                _constructorInfoInductive = ind,
+                _constructorInfoBuiltin = builtin
+              }
+          )
           | StatementInductive d <- ss,
             let ind = d ^. inductiveName,
-            c <- d ^. inductiveConstructors,
+            let n = length (d ^. inductiveConstructors),
+            let builtins = maybe (replicate n Nothing) (map Just . builtinConstructors) (d ^. inductiveBuiltin),
+            (builtin, c) <- zipExact builtins (d ^. inductiveConstructors),
             let args = c ^. constructorParameters
         ]
     _infoFunctions :: HashMap Name FunctionInfo
     _infoFunctions =
       HashMap.fromList
-        [ (f ^. funDefName, FunctionInfo (f ^. funDefType) (length (head (f ^. funDefClauses) ^. clausePatterns)))
+        [ ( f ^. funDefName,
+            FunctionInfo
+              { _functionInfoType = f ^. funDefType,
+                _functionInfoPatterns = length (head (f ^. funDefClauses) ^. clausePatterns),
+                _functionInfoBuiltin = f ^. funDefBuiltin
+              }
+          )
           | StatementFunction f <- ss
         ]
     _infoAxioms :: HashMap Name AxiomInfo
     _infoAxioms =
       HashMap.fromList
-        [ (d ^. axiomName, AxiomInfo (d ^. axiomType))
+        [ ( d ^. axiomName,
+            AxiomInfo
+              { _axiomInfoType = d ^. axiomType,
+                _axiomInfoBuiltin = d ^. axiomBuiltin
+              }
+          )
           | StatementAxiom d <- ss
         ]
     ss = m ^. (moduleBody . moduleStatements)
@@ -53,4 +86,17 @@ buildTable m = InfoTable {..}
 makeLenses ''InfoTable
 makeLenses ''FunctionInfo
 makeLenses ''ConstructorInfo
+makeLenses ''InductiveInfo
 makeLenses ''AxiomInfo
+
+lookupConstructor :: Member (Reader InfoTable) r => Name -> Sem r ConstructorInfo
+lookupConstructor c = asks (^?! infoConstructors . at c . _Just)
+
+lookupInductive :: Member (Reader InfoTable) r => Name -> Sem r InductiveInfo
+lookupInductive c = asks (^?! infoInductives . at c . _Just)
+
+lookupFunction :: Member (Reader InfoTable) r => Name -> Sem r FunctionInfo
+lookupFunction c = asks (^?! infoFunctions . at c . _Just)
+
+lookupAxiom :: Member (Reader InfoTable) r => Name -> Sem r AxiomInfo
+lookupAxiom c = asks (^?! infoAxioms . at c . _Just)
diff --git a/src/MiniJuvix/Syntax/MonoJuvix/Language.hs b/src/MiniJuvix/Syntax/MonoJuvix/Language.hs
index 57c2ef1d14..60c675b871 100644
--- a/src/MiniJuvix/Syntax/MonoJuvix/Language.hs
+++ b/src/MiniJuvix/Syntax/MonoJuvix/Language.hs
@@ -2,51 +2,18 @@ module MiniJuvix.Syntax.MonoJuvix.Language
   ( module MiniJuvix.Syntax.MonoJuvix.Language,
     module MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind,
     module MiniJuvix.Syntax.Concrete.Scoped.Name,
+    module MiniJuvix.Syntax.Abstract.Name,
+    module MiniJuvix.Syntax.Concrete.Builtins,
   )
 where
 
 import MiniJuvix.Prelude
+import MiniJuvix.Syntax.Abstract.Name
+import MiniJuvix.Syntax.Concrete.Builtins
 import MiniJuvix.Syntax.Concrete.Language qualified as C
 import MiniJuvix.Syntax.Concrete.Scoped.Name (NameId (..))
 import MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind
-import MiniJuvix.Syntax.Fixity
 import MiniJuvix.Syntax.ForeignBlock
-import Prettyprinter
-
-type FunctionName = Name
-
-type AxiomName = Name
-
-type VarName = Name
-
-type ConstrName = Name
-
-type InductiveName = Name
-
-data Name = Name
-  { _nameText :: Text,
-    _nameId :: NameId,
-    _nameKind :: NameKind,
-    _nameLoc :: C.Interval
-  }
-  deriving stock (Show)
-
-makeLenses ''Name
-
-instance Eq Name where
-  (==) = (==) `on` (^. nameId)
-
-instance Ord Name where
-  compare = compare `on` (^. nameId)
-
-instance Hashable Name where
-  hashWithSalt salt = hashWithSalt salt . (^. nameId)
-
-instance HasNameKind Name where
-  getNameKind = (^. nameKind)
-
-instance Pretty Name where
-  pretty = pretty . (^. nameText)
 
 data Module = Module
   { _moduleName :: Name,
@@ -65,13 +32,15 @@ data Statement
 
 data AxiomDef = AxiomDef
   { _axiomName :: AxiomName,
+    _axiomBuiltin :: Maybe BuiltinAxiom,
     _axiomType :: Type
   }
 
 data FunctionDef = FunctionDef
   { _funDefName :: FunctionName,
     _funDefType :: Type,
-    _funDefClauses :: NonEmpty FunctionClause
+    _funDefClauses :: NonEmpty FunctionClause,
+    _funDefBuiltin :: Maybe BuiltinFunction
   }
 
 data FunctionClause = FunctionClause
@@ -128,6 +97,7 @@ data Pattern
 
 data InductiveDef = InductiveDef
   { _inductiveName :: InductiveName,
+    _inductiveBuiltin :: Maybe BuiltinInductive,
     _inductiveConstructors :: [InductiveConstructorDef]
   }
 
diff --git a/src/MiniJuvix/Syntax/MonoJuvix/MonoJuvixResult.hs b/src/MiniJuvix/Syntax/MonoJuvix/MonoJuvixResult.hs
index 3f2269ce8e..7bf7794c19 100644
--- a/src/MiniJuvix/Syntax/MonoJuvix/MonoJuvixResult.hs
+++ b/src/MiniJuvix/Syntax/MonoJuvix/MonoJuvixResult.hs
@@ -31,10 +31,10 @@ compileInfoTable r =
     (^. Scoper.nameId)
     ( r
         ^. resultMicroTyped
-          . Micro.resultMicroJuvixArityResult
-          . Micro.resultMicroJuvixResult
-          . Micro.resultAbstract
-          . Abstract.resultScoper
-          . Scoper.resultScoperTable
-          . Scoper.infoCompilationRules
+        . Micro.resultMicroJuvixArityResult
+        . Micro.resultMicroJuvixResult
+        . Micro.resultAbstract
+        . Abstract.resultScoper
+        . Scoper.resultScoperTable
+        . Scoper.infoCompilationRules
     )
diff --git a/src/MiniJuvix/Syntax/MonoJuvix/Pretty/Base.hs b/src/MiniJuvix/Syntax/MonoJuvix/Pretty/Base.hs
index bb7608ac01..1fd1b36e24 100644
--- a/src/MiniJuvix/Syntax/MonoJuvix/Pretty/Base.hs
+++ b/src/MiniJuvix/Syntax/MonoJuvix/Pretty/Base.hs
@@ -39,9 +39,10 @@ instance PrettyCode Name where
       if
           | showNameId -> Just . ("@" <>) <$> ppCode (n ^. nameId)
           | otherwise -> return Nothing
-    return $
-      annotate (AnnKind (n ^. nameKind)) $
-        pretty (n ^. nameText) <?> uid
+    return
+      $ annotate (AnnKind (n ^. nameKind))
+      $ pretty (n ^. nameText)
+      <?> uid
 
 instance PrettyCode Iden where
   ppCode :: Member (Reader Options) r => Iden -> Sem r (Doc Ann)
@@ -181,8 +182,11 @@ instance PrettyCode FunctionDef where
     funDefType' <- ppCode (f ^. funDefType)
     clauses' <- mapM ppCode (f ^. funDefClauses)
     return $
-      funDefName' <+> kwColonColon <+> funDefType' <> line
-        <> vsep (toList clauses')
+      funDefName'
+        <+> kwColonColon
+        <+> funDefType'
+          <> line
+          <> vsep (toList clauses')
 
 instance PrettyCode FunctionClause where
   ppCode c = do
@@ -200,10 +204,13 @@ instance PrettyCode ForeignBlock where
   ppCode ForeignBlock {..} = do
     _foreignBackend' <- ppCode _foreignBackend
     return $
-      kwForeign <+> _foreignBackend' <+> lbrace <> line
-        <> pretty _foreignCode
-        <> line
-        <> rbrace
+      kwForeign
+        <+> _foreignBackend'
+        <+> lbrace
+          <> line
+          <> pretty _foreignCode
+          <> line
+          <> rbrace
 
 instance PrettyCode AxiomDef where
   ppCode AxiomDef {..} = do
@@ -228,11 +235,13 @@ instance PrettyCode Module where
     name' <- ppCode (m ^. moduleName)
     body' <- ppCode (m ^. moduleBody)
     return $
-      kwModule <+> name' <+> kwWhere
-        <> line
-        <> line
-        <> body'
-        <> line
+      kwModule
+        <+> name'
+        <+> kwWhere
+          <> line
+          <> line
+          <> body'
+          <> line
 
 parensCond :: Bool -> Doc Ann -> Doc Ann
 parensCond t d = if t then parens d else d
diff --git a/src/MiniJuvix/Syntax/Universe.hs b/src/MiniJuvix/Syntax/Universe.hs
index 0e787a77f5..1234eda195 100644
--- a/src/MiniJuvix/Syntax/Universe.hs
+++ b/src/MiniJuvix/Syntax/Universe.hs
@@ -6,9 +6,23 @@ import MiniJuvix.Syntax.Fixity
 newtype Universe = Universe
   { _universeLevel :: Maybe Natural
   }
-  deriving stock (Show, Eq, Ord)
+  deriving stock (Show, Ord)
 
-instance HasAtomicity Universe where
-  atomicity = const Atom
+instance Eq Universe where
+  (Universe a) == (Universe b) = f a == f b
+    where
+      f :: Maybe Natural -> Natural
+      f = fromMaybe defaultLevel
+
+smallUniverse :: Universe
+smallUniverse = Universe (Just 0)
+
+defaultLevel :: Natural
+defaultLevel = 0
 
 makeLenses ''Universe
+
+instance HasAtomicity Universe where
+  atomicity u = case u ^. universeLevel of
+    Nothing -> Atom
+    Just {} -> Aggregate appFixity
diff --git a/src/MiniJuvix/Termination/Error/Pretty/Ansi.hs b/src/MiniJuvix/Termination/Error/Pretty/Ansi.hs
index 74e1773c23..c4435e0720 100644
--- a/src/MiniJuvix/Termination/Error/Pretty/Ansi.hs
+++ b/src/MiniJuvix/Termination/Error/Pretty/Ansi.hs
@@ -14,5 +14,5 @@ renderAnsi = renderStrict . reAnnotateS stylize
 
 stylize :: Eann -> AnsiStyle
 stylize a = case a of
-  Highlight -> colorDull Red
+  Highlight -> bold
   AbstractAnn m -> M.stylize m
diff --git a/src/MiniJuvix/Termination/Error/Types.hs b/src/MiniJuvix/Termination/Error/Types.hs
index 935ba3c07d..9d192a72c1 100644
--- a/src/MiniJuvix/Termination/Error/Types.hs
+++ b/src/MiniJuvix/Termination/Error/Types.hs
@@ -25,5 +25,6 @@ instance ToGenericError NoLexOrder where
 
       msg :: Doc Eann
       msg =
-        "The function" <+> highlight (pretty name)
+        "The function"
+          <+> highlight (pretty name)
           <+> "fails the termination checker."
diff --git a/src/MiniJuvix/Termination/Types/Graph.hs b/src/MiniJuvix/Termination/Types/Graph.hs
index 1b639a3063..a5b2b40d83 100644
--- a/src/MiniJuvix/Termination/Types/Graph.hs
+++ b/src/MiniJuvix/Termination/Types/Graph.hs
@@ -45,8 +45,12 @@ instance PrettyCode Edge where
       indent 2 . ppMatrices . zip [0 :: Int ..]
         <$> mapM ppCode (toList _edgeMatrices)
     return $
-      pretty ("Edge" :: Text) <+> fromFun <+> kwWaveArrow <+> toFun <> line
-        <> matrices
+      pretty ("Edge" :: Text)
+        <+> fromFun
+        <+> kwWaveArrow
+        <+> toFun
+          <> line
+          <> matrices
     where
       ppMatrices :: [(Int, Doc a)] -> Doc a
       ppMatrices = vsep2 . map ppMatrix
@@ -68,7 +72,10 @@ instance PrettyCode RecursiveBehaviour where
     f' <- ppCode f
     let m' = PP.vsep (map (PP.list . map pretty) m)
     return $
-      pretty ("Recursive behaviour of" :: Text) <+> f' <> colon <> line
-        <> indent 2 (align m')
+      pretty ("Recursive behaviour of" :: Text)
+        <+> f'
+          <> colon
+          <> line
+          <> indent 2 (align m')
     where
       m = toList (HashSet.fromList m0)
diff --git a/src/MiniJuvix/Translation/AbstractToMicroJuvix.hs b/src/MiniJuvix/Translation/AbstractToMicroJuvix.hs
index e830a19cf1..e2fc46096f 100644
--- a/src/MiniJuvix/Translation/AbstractToMicroJuvix.hs
+++ b/src/MiniJuvix/Translation/AbstractToMicroJuvix.hs
@@ -60,7 +60,7 @@ entryMicroJuvix abstractResults = do
     noTerminationOption =
       abstractResults
         ^. Abstract.abstractResultEntryPoint
-          . E.entryPointNoTermination
+        . E.entryPointNoTermination
 
 goModule ::
   Members '[State TranslationState, Error TypeCheckerError] r =>
@@ -121,6 +121,7 @@ goAxiomDef a = do
   return
     AxiomDef
       { _axiomName = a ^. Abstract.axiomName,
+        _axiomBuiltin = a ^. Abstract.axiomBuiltin,
         _axiomType = _axiomType'
       }
 
@@ -162,7 +163,8 @@ goFunctionDef f = do
     FunctionDef
       { _funDefName = _funDefName',
         _funDefType = _funDefType',
-        _funDefClauses = _funDefClauses'
+        _funDefClauses = _funDefClauses',
+        _funDefBuiltin = f ^. Abstract.funDefBuiltin
       }
   where
     _funDefName' :: Name
@@ -265,80 +267,76 @@ goInductiveParameter f =
     (Just {}, _, _) -> unsupported "only type variables of small types are allowed"
     (Nothing, _, _) -> unsupported "unnamed inductive parameters"
 
-goConstructorType :: Abstract.Expression -> Sem r [Type]
-goConstructorType = fmap fst . viewConstructorType
-
 goInductiveDef ::
   forall r.
-  Members '[Error TypeCheckerError] r =>
+  Member (Error TypeCheckerError) r =>
   Abstract.InductiveDef ->
   Sem r InductiveDef
-goInductiveDef i = case i ^. Abstract.inductiveType of
-  Just Abstract.ExpressionUniverse {} -> helper
-  Just {} -> unsupported "inductive indices"
-  _ -> helper
+goInductiveDef i =
+  if
+      | not (isSmallType (i ^. Abstract.inductiveType)) -> unsupported "inductive indices"
+      | otherwise -> do
+          inductiveParameters' <- mapM goInductiveParameter (i ^. Abstract.inductiveParameters)
+          let indTypeName = i ^. Abstract.inductiveName
+              indParamNames = map (^. inductiveParamName) inductiveParameters'
+          inductiveConstructors' <- mapM (goConstructorDef indTypeName indParamNames) (i ^. Abstract.inductiveConstructors)
+          return
+            InductiveDef
+              { _inductiveName = indTypeName,
+                _inductiveParameters = inductiveParameters',
+                _inductiveBuiltin = i ^. Abstract.inductiveBuiltin,
+                _inductiveConstructors = inductiveConstructors'
+              }
   where
-    helper = do
-      inductiveParameters' <- mapM goInductiveParameter (i ^. Abstract.inductiveParameters)
-      let indTypeName = i ^. Abstract.inductiveName
-          indParamNames = map (^. inductiveParamName) inductiveParameters'
-      inductiveConstructors' <- mapM (goConstructorDef indTypeName indParamNames) (i ^. Abstract.inductiveConstructors)
-      return
-        InductiveDef
-          { _inductiveName = indTypeName,
-            _inductiveParameters = inductiveParameters',
-            _inductiveConstructors = inductiveConstructors'
-          }
-      where
-        goConstructorDef :: Name -> [Name] -> Abstract.InductiveConstructorDef -> Sem r InductiveConstructorDef
-        goConstructorDef expectedTypeName expectedNameParms c = do
-          (_constructorParameters', actualReturnType) <- viewConstructorType (c ^. Abstract.constructorType)
-          let ctorName = c ^. Abstract.constructorName
-              expectedReturnType :: Type
-              expectedReturnType = foldTypeAppName expectedTypeName expectedNameParms
-              expectedNumArgs = length expectedNameParms
-              (_, actualReturnTypeParams) = unfoldType actualReturnType
-              actualNumArgs = length actualReturnTypeParams
-              sameTypeName = Just expectedTypeName == getTypeName actualReturnType
-          if
-              | actualReturnType == expectedReturnType ->
-                  return
-                    InductiveConstructorDef
-                      { _constructorName = ctorName,
-                        _constructorParameters = _constructorParameters'
-                      }
-              | sameTypeName,
-                actualNumArgs < expectedNumArgs ->
-                  throw
-                    ( ErrTooFewArgumentsIndType
-                        ( WrongNumberArgumentsIndType
-                            { _wrongNumberArgumentsIndTypeActualType = actualReturnType,
-                              _wrongNumberArgumentsIndTypeActualNumArgs = actualNumArgs,
-                              _wrongNumberArgumentsIndTypeExpectedNumArgs = expectedNumArgs
-                            }
-                        )
+    goConstructorDef :: Name -> [Name] -> Abstract.InductiveConstructorDef -> Sem r InductiveConstructorDef
+    goConstructorDef expectedTypeName expectedNameParms c = do
+      (_constructorParameters', actualReturnType) <- viewConstructorType (c ^. Abstract.constructorType)
+      let ctorName = c ^. Abstract.constructorName
+          expectedReturnType :: Type
+          expectedReturnType = foldTypeAppName expectedTypeName expectedNameParms
+          expectedNumArgs = length expectedNameParms
+          (_, actualReturnTypeParams) = unfoldType actualReturnType
+          actualNumArgs = length actualReturnTypeParams
+          sameTypeName = Just expectedTypeName == getTypeName actualReturnType
+      if
+          | actualReturnType == expectedReturnType ->
+              return
+                InductiveConstructorDef
+                  { _constructorName = ctorName,
+                    _constructorParameters = _constructorParameters'
+                  }
+          | sameTypeName,
+            actualNumArgs < expectedNumArgs ->
+              throw
+                ( ErrTooFewArgumentsIndType
+                    ( WrongNumberArgumentsIndType
+                        { _wrongNumberArgumentsIndTypeActualType = actualReturnType,
+                          _wrongNumberArgumentsIndTypeActualNumArgs = actualNumArgs,
+                          _wrongNumberArgumentsIndTypeExpectedNumArgs = expectedNumArgs
+                        }
                     )
-              | sameTypeName,
-                actualNumArgs > expectedNumArgs ->
-                  throw
-                    ( ErrTooManyArgumentsIndType
-                        ( WrongNumberArgumentsIndType
-                            { _wrongNumberArgumentsIndTypeActualType = actualReturnType,
-                              _wrongNumberArgumentsIndTypeActualNumArgs = actualNumArgs,
-                              _wrongNumberArgumentsIndTypeExpectedNumArgs = expectedNumArgs
-                            }
-                        )
+                )
+          | sameTypeName,
+            actualNumArgs > expectedNumArgs ->
+              throw
+                ( ErrTooManyArgumentsIndType
+                    ( WrongNumberArgumentsIndType
+                        { _wrongNumberArgumentsIndTypeActualType = actualReturnType,
+                          _wrongNumberArgumentsIndTypeActualNumArgs = actualNumArgs,
+                          _wrongNumberArgumentsIndTypeExpectedNumArgs = expectedNumArgs
+                        }
                     )
-              | otherwise ->
-                  throw
-                    ( ErrWrongReturnType
-                        ( WrongReturnType
-                            { _wrongReturnTypeConstructorName = ctorName,
-                              _wrongReturnTypeExpected = expectedReturnType,
-                              _wrongReturnTypeActual = actualReturnType
-                            }
-                        )
+                )
+          | otherwise ->
+              throw
+                ( ErrWrongReturnType
+                    ( WrongReturnType
+                        { _wrongReturnTypeConstructorName = ctorName,
+                          _wrongReturnTypeExpected = expectedReturnType,
+                          _wrongReturnTypeActual = actualReturnType
+                        }
                     )
+                )
 
 goTypeApplication :: Abstract.Application -> Sem r TypeApplication
 goTypeApplication (Abstract.Application l r i) = do
diff --git a/src/MiniJuvix/Translation/MicroJuvixToMonoJuvix.hs b/src/MiniJuvix/Translation/MicroJuvixToMonoJuvix.hs
index db84a279ef..39781b7e88 100644
--- a/src/MiniJuvix/Translation/MicroJuvixToMonoJuvix.hs
+++ b/src/MiniJuvix/Translation/MicroJuvixToMonoJuvix.hs
@@ -195,9 +195,11 @@ goStatement = \case
 goAxiomDef :: Members '[Reader ConcreteTable] r => Micro.AxiomDef -> Sem r AxiomDef
 goAxiomDef Micro.AxiomDef {..} = do
   _axiomType' <- goType (Micro.mkConcreteType' _axiomType)
+  let _axiomBuiltin' = _axiomBuiltin
   return
     AxiomDef
       { _axiomName = goName _axiomName,
+        _axiomBuiltin = _axiomBuiltin',
         _axiomType = _axiomType'
       }
 
@@ -265,6 +267,7 @@ goInductiveDefConcrete def = do
   return
     InductiveDef
       { _inductiveName = goName (def ^. Micro.inductiveName),
+        _inductiveBuiltin = def ^. Micro.inductiveBuiltin,
         _inductiveConstructors = constructors'
       }
   where
@@ -341,7 +344,8 @@ goFunctionDefConcrete n d = do
     FunctionDef
       { _funDefName = funName,
         _funDefClauses = clauses',
-        _funDefType = type'
+        _funDefType = type',
+        _funDefBuiltin = d ^. Micro.funDefBuiltin
       }
   where
     funName :: Name
@@ -377,6 +381,7 @@ goInductiveDefPoly def poly
       return
         InductiveDef
           { _inductiveName = i ^. concreteName,
+            _inductiveBuiltin = Nothing,
             ..
           }
       where
@@ -417,7 +422,8 @@ goFunctionDefPoly def poly
         Micro.FunctionDef
           { _funDefName = impossible,
             _funDefType = sig' ^. Micro.unconcreteType,
-            _funDefClauses = _funDefClauses
+            _funDefClauses = _funDefClauses,
+            _funDefBuiltin = def ^. Micro.funDefBuiltin
           }
       where
         concreteSubs :: Micro.ConcreteSubs
diff --git a/src/MiniJuvix/Translation/MonoJuvixToMiniC.hs b/src/MiniJuvix/Translation/MonoJuvixToMiniC.hs
index 244842c776..1373936c88 100644
--- a/src/MiniJuvix/Translation/MonoJuvixToMiniC.hs
+++ b/src/MiniJuvix/Translation/MonoJuvixToMiniC.hs
@@ -5,6 +5,7 @@ module MiniJuvix.Translation.MonoJuvixToMiniC
 where
 
 import Data.HashMap.Strict qualified as HashMap
+import MiniJuvix.Builtins
 import MiniJuvix.Internal.Strings qualified as Str
 import MiniJuvix.Prelude
 import MiniJuvix.Syntax.Backends
@@ -17,20 +18,23 @@ import MiniJuvix.Syntax.MonoJuvix.Language qualified as Mono
 import MiniJuvix.Syntax.NameId
 import MiniJuvix.Translation.MicroJuvixToMonoJuvix qualified as Mono
 import MiniJuvix.Translation.MonoJuvixToMiniC.Base
+import MiniJuvix.Translation.MonoJuvixToMiniC.BuiltinTable
 import MiniJuvix.Translation.MonoJuvixToMiniC.Closure
 import MiniJuvix.Translation.MonoJuvixToMiniC.Types
 
-entryMiniC :: Mono.MonoJuvixResult -> Sem r MiniCResult
-entryMiniC i = return (MiniCResult (serialize cunitResult))
+entryMiniC :: forall r. Member Builtins r => Mono.MonoJuvixResult -> Sem r MiniCResult
+entryMiniC i = MiniCResult . serialize <$> cunitResult
   where
     compileInfo :: Mono.CompileInfoTable
     compileInfo = Mono.compileInfoTable i
 
-    cunitResult :: CCodeUnit
-    cunitResult =
-      CCodeUnit
-        { _ccodeCode = cheader <> cmodules
-        }
+    cunitResult :: Sem r CCodeUnit
+    cunitResult = do
+      cmodules' <- cmodules
+      return
+        CCodeUnit
+          { _ccodeCode = cheader <> cmodules'
+          }
 
     cheader :: [CCode]
     cheader =
@@ -40,16 +44,20 @@ entryMiniC i = return (MiniCResult (serialize cunitResult))
           CppIncludeFile Str.minicRuntime
         ]
 
-    cmodules :: [CCode]
-    cmodules = do
-      m <- toList (i ^. Mono.resultModules)
+    cmodule :: Mono.Module -> Sem r [CCode]
+    cmodule m = do
       let buildTable = Mono.buildTable m
-      genStructDefs m
-        <> run (runReader compileInfo (genAxioms m))
-        <> genCTypes m
-        <> genFunctionSigs m
-        <> run (runReader buildTable (genClosures m))
-        <> run (runReader buildTable (genFunctionDefs m))
+      let defs =
+            genStructDefs m
+              <> run (runReader compileInfo (genAxioms m))
+              <> run (runReader buildTable (genCTypes m))
+              <> run (runReader buildTable (genFunctionSigs m))
+              <> run (runReader buildTable (genClosures m))
+      funDefs <- runReader buildTable (genFunctionDefs m)
+      return (defs <> funDefs)
+
+    cmodules :: Sem r [CCode]
+    cmodules = concatMapM cmodule (toList (i ^. Mono.resultModules))
 
 genStructDefs :: Mono.Module -> [CCode]
 genStructDefs Mono.Module {..} =
@@ -71,29 +79,29 @@ genAxioms Mono.Module {..} =
       Mono.StatementForeign {} -> return []
       Mono.StatementFunction {} -> return []
 
-genCTypes :: Mono.Module -> [CCode]
+genCTypes :: forall r. Member (Reader Mono.InfoTable) r => Mono.Module -> Sem r [CCode]
 genCTypes Mono.Module {..} =
-  concatMap go (_moduleBody ^. Mono.moduleStatements)
+  concatMapM go (_moduleBody ^. Mono.moduleStatements)
   where
-    go :: Mono.Statement -> [CCode]
+    go :: Mono.Statement -> Sem r [CCode]
     go = \case
       Mono.StatementInductive d -> goInductiveDef d
-      Mono.StatementAxiom {} -> []
-      Mono.StatementForeign d -> goForeign d
-      Mono.StatementFunction {} -> []
+      Mono.StatementAxiom {} -> return []
+      Mono.StatementForeign d -> return (goForeign d)
+      Mono.StatementFunction {} -> return []
 
-genFunctionSigs :: Mono.Module -> [CCode]
+genFunctionSigs :: forall r. Member (Reader Mono.InfoTable) r => Mono.Module -> Sem r [CCode]
 genFunctionSigs Mono.Module {..} =
-  applyOnFunStatement genFunctionSig =<< _moduleBody ^. Mono.moduleStatements
+  concatMapM (applyOnFunStatement genFunctionSig) (_moduleBody ^. Mono.moduleStatements)
 
 genFunctionDefs ::
-  Members '[Reader Mono.InfoTable] r =>
+  Members '[Reader Mono.InfoTable, Builtins] r =>
   Mono.Module ->
   Sem r [CCode]
 genFunctionDefs Mono.Module {..} = genFunctionDefsBody _moduleBody
 
 genFunctionDefsBody ::
-  Members '[Reader Mono.InfoTable] r =>
+  Members '[Reader Mono.InfoTable, Builtins] r =>
   Mono.ModuleBody ->
   Sem r [CCode]
 genFunctionDefsBody Mono.ModuleBody {..} =
@@ -102,99 +110,108 @@ genFunctionDefsBody Mono.ModuleBody {..} =
 isNullary :: Text -> CFunType -> Bool
 isNullary funName funType = null (funType ^. cFunArgTypes) && funName /= Str.main_
 
-mkFunctionSig :: Mono.FunctionDef -> FunctionSig
+mkFunctionSig :: forall r. Member (Reader Mono.InfoTable) r => Mono.FunctionDef -> Sem r FunctionSig
 mkFunctionSig Mono.FunctionDef {..} =
-  cFunTypeToFunSig funName funType
+  cFunTypeToFunSig <$> funName <*> funType
   where
     -- Assumption: All clauses have the same number of patterns
     nPatterns :: Int
     nPatterns = length (head _funDefClauses ^. Mono.clausePatterns)
 
-    baseFunType :: CFunType
+    baseFunType :: Sem r CFunType
     baseFunType = typeToFunType _funDefType
 
-    funType :: CFunType
-    funType =
-      if
-          | nPatterns == length (baseFunType ^. cFunArgTypes) -> baseFunType
-          | otherwise ->
+    funType :: Sem r CFunType
+    funType = do
+      typ <- baseFunType
+      return
+        ( if nPatterns == length (typ ^. cFunArgTypes)
+            then typ
+            else
               CFunType
-                { _cFunArgTypes = take nPatterns (baseFunType ^. cFunArgTypes),
+                { _cFunArgTypes = take nPatterns (typ ^. cFunArgTypes),
                   _cFunReturnType = declFunctionPtrType
                 }
+        )
 
-    funIsNullary :: Bool
-    funIsNullary = isNullary funcBasename funType
+    funIsNullary :: Sem r Bool
+    funIsNullary = isNullary funcBasename <$> funType
 
     funcBasename :: Text
     funcBasename = mkName _funDefName
 
-    funName :: Text
-    funName =
-      if
-          | funIsNullary -> asNullary funcBasename
-          | otherwise -> funcBasename
-
-genFunctionSig :: Mono.FunctionDef -> [CCode]
-genFunctionSig d@(Mono.FunctionDef {..}) =
-  [ExternalFuncSig (mkFunctionSig d)]
-    <> (ExternalMacro . CppDefineParens <$> toList nullaryDefine)
+    funName :: Sem r Text
+    funName = bool funcBasename (asNullary funcBasename) <$> funIsNullary
+
+genFunctionSig :: forall r. Member (Reader Mono.InfoTable) r => Mono.FunctionDef -> Sem r [CCode]
+genFunctionSig d@(Mono.FunctionDef {..}) = do
+  sig <- mkFunctionSig d
+  nullaryDefine' <- nullaryDefine
+  return
+    ( [ExternalFuncSig sig]
+        <> (ExternalMacro . CppDefineParens <$> toList nullaryDefine')
+    )
   where
     nPatterns :: Int
     nPatterns = length (head _funDefClauses ^. Mono.clausePatterns)
 
-    baseFunType :: CFunType
+    baseFunType :: Sem r CFunType
     baseFunType = typeToFunType _funDefType
 
-    funType :: CFunType
-    funType =
-      if
-          | nPatterns == length (baseFunType ^. cFunArgTypes) -> baseFunType
-          | otherwise ->
+    funType :: Sem r CFunType
+    funType = do
+      typ <- baseFunType
+      return
+        ( if nPatterns == length (typ ^. cFunArgTypes)
+            then typ
+            else
               CFunType
-                { _cFunArgTypes = take nPatterns (baseFunType ^. cFunArgTypes),
+                { _cFunArgTypes = take nPatterns (typ ^. cFunArgTypes),
                   _cFunReturnType = declFunctionPtrType
                 }
+        )
 
-    funIsNullary :: Bool
-    funIsNullary = isNullary funcBasename funType
+    funIsNullary :: Sem r Bool
+    funIsNullary = isNullary funcBasename <$> funType
 
     funcBasename :: Text
     funcBasename = mkName _funDefName
 
-    funName :: Text
-    funName =
-      if
-          | funIsNullary -> asNullary funcBasename
-          | otherwise -> funcBasename
-
-    nullaryDefine :: Maybe Define
-    nullaryDefine =
-      if
-          | funIsNullary ->
-              Just $
-                Define
-                  { _defineName = funcBasename,
-                    _defineBody = functionCall (ExpressionVar funName) []
-                  }
-          | otherwise -> Nothing
+    funName :: Sem r Text
+    funName = bool funcBasename (asNullary funcBasename) <$> funIsNullary
+
+    nullaryDefine :: Sem r (Maybe Define)
+    nullaryDefine = do
+      n <- funName
+      bool
+        Nothing
+        ( Just $
+            Define
+              { _defineName = funcBasename,
+                _defineBody = functionCall (ExpressionVar n) []
+              }
+        )
+        <$> funIsNullary
 
 goFunctionDef ::
-  Members '[Reader Mono.InfoTable] r =>
+  Members '[Reader Mono.InfoTable, Builtins] r =>
   Mono.FunctionDef ->
   Sem r [CCode]
-goFunctionDef d@(Mono.FunctionDef {..}) = do
-  fc <- mapM (goFunctionClause (fst (unfoldFunType _funDefType))) (toList _funDefClauses)
-  let bodySpec = fst <$> fc
-  let preDecls :: [Function] = snd =<< fc
-  return $
-    (ExternalFunc <$> preDecls)
-      <> [ ExternalFunc $
-             Function
-               { _funcSig = mkFunctionSig d,
-                 _funcBody = maybeToList (BodyStatement <$> mkBody bodySpec)
-               }
-         ]
+goFunctionDef d@(Mono.FunctionDef {..})
+  | isJust _funDefBuiltin = return []
+  | otherwise = do
+      fc <- mapM (goFunctionClause (fst (unfoldFunType _funDefType))) (toList _funDefClauses)
+      let bodySpec = fst <$> fc
+      let preDecls :: [Function] = snd =<< fc
+      funSig <- mkFunctionSig d
+      return $
+        (ExternalFunc <$> preDecls)
+          <> [ ExternalFunc $
+                 Function
+                   { _funcSig = funSig,
+                     _funcBody = maybeToList (BodyStatement <$> mkBody bodySpec)
+                   }
+             ]
   where
     mkBody :: [(Maybe Expression, Statement)] -> Maybe Statement
     mkBody cs = do
@@ -224,7 +241,8 @@ goFunctionDef d@(Mono.FunctionDef {..}) = do
                 [ ExpressionLiteral
                     ( LiteralString
                         ( "Error: Pattern match(es) are non-exhaustive in "
-                            <> (_funDefName ^. Mono.nameText)
+                            <> _funDefName
+                            ^. Mono.nameText
                         )
                     )
                 ]
@@ -239,43 +257,40 @@ goFunctionDef d@(Mono.FunctionDef {..}) = do
 
 goFunctionClause ::
   forall r.
-  Members '[Reader Mono.InfoTable] r =>
+  Members '[Reader Mono.InfoTable, Builtins] r =>
   [Mono.Type] ->
   Mono.FunctionClause ->
   Sem r ((Maybe Expression, Statement), [Function])
 goFunctionClause argTyps clause = do
   (stmt, decls) <- returnStmt
-  return ((clauseCondition, stmt), decls)
+  cond <- clauseCondition
+  return ((cond, stmt), decls)
   where
-    conditions :: [Expression]
-    conditions = do
-      (p, arg) <- zip (clause ^. Mono.clausePatterns) funArgs
-      patternCondition (ExpressionVar arg) p
-
-    patternCondition :: Expression -> Mono.Pattern -> [Expression]
+    conditions :: Sem r [Expression]
+    conditions =
+      concat
+        <$> sequence
+          [ patternCondition (ExpressionVar arg) p
+            | (p, arg) <- zip (clause ^. Mono.clausePatterns) funArgs
+          ]
+
+    patternCondition :: Expression -> Mono.Pattern -> Sem r [Expression]
     patternCondition arg = \case
-      Mono.PatternConstructorApp Mono.ConstructorApp {..} ->
-        isCtor : subConditions
-        where
-          ctorName :: Text
-          ctorName = mkName _constrAppConstructor
-
-          isCtor :: Expression
-          isCtor = functionCall (ExpressionVar (asIs ctorName)) [arg]
-
-          asCtor :: Expression
-          asCtor = functionCall (ExpressionVar (asCast ctorName)) [arg]
-          subConditions :: [Expression]
-
-          subConditions = do
-            let subArgs = map (memberAccess Object asCtor) ctorArgs
-            (p, subArg) <- zip _constrAppParameters subArgs
-            patternCondition subArg p
-      Mono.PatternVariable {} -> []
-      Mono.PatternWildcard {} -> []
-
-    clauseCondition :: Maybe Expression
-    clauseCondition = fmap (foldr1 f) (nonEmpty conditions)
+      Mono.PatternConstructorApp Mono.ConstructorApp {..} -> do
+        ctorName <- getConstructorCName _constrAppConstructor
+
+        let isCtor :: Expression
+            isCtor = functionCall (ExpressionVar (asIs ctorName)) [arg]
+            projCtor :: Text -> Expression
+            projCtor ctorArg = functionCall (ExpressionVar (asProjName ctorArg ctorName)) [arg]
+            subConditions :: Sem r [Expression]
+            subConditions = fmap concat (zipWithM patternCondition (map projCtor ctorArgs) _constrAppParameters)
+        fmap (isCtor :) subConditions
+      Mono.PatternVariable {} -> return []
+      Mono.PatternWildcard {} -> return []
+
+    clauseCondition :: Sem r (Maybe Expression)
+    clauseCondition = fmap (foldr1 f) . nonEmpty <$> conditions
       where
         f :: Expression -> Expression -> Expression
         f e1 e2 =
@@ -292,7 +307,7 @@ goFunctionClause argTyps clause = do
       (decls :: [Function], clauseResult) <- runOutputList (runReader bindings (goExpression (clause ^. Mono.clauseBody)))
       return (StatementReturn (Just clauseResult), decls)
 
-goExpression :: Members '[Reader Mono.InfoTable, Reader PatternInfoTable] r => Mono.Expression -> Sem r Expression
+goExpression :: Members '[Reader Mono.InfoTable, Builtins, Reader PatternInfoTable] r => Mono.Expression -> Sem r Expression
 goExpression = \case
   Mono.ExpressionIden i -> do
     let rootFunMonoName = Mono.getName i
@@ -303,21 +318,24 @@ goExpression = \case
       _ -> do
         (t, _) <- getType i
         let argTyps = t ^. cFunArgTypes
-        if
-            | null argTyps -> goIden i
-            | otherwise -> return $ functionCall (ExpressionVar evalFunName) []
+        (if null argTyps then goIden i else return $ functionCall (ExpressionVar evalFunName) [])
   Mono.ExpressionApplication a -> goApplication a
   Mono.ExpressionLiteral l -> return (ExpressionLiteral (goLiteral l))
 
-goIden :: Members '[Reader PatternInfoTable, Reader Mono.InfoTable] r => Mono.Iden -> Sem r Expression
+goIden :: Members '[Reader PatternInfoTable, Builtins, Reader Mono.InfoTable] r => Mono.Iden -> Sem r Expression
 goIden = \case
-  Mono.IdenFunction n -> return (ExpressionVar (mkName n))
-  Mono.IdenConstructor n -> return (ExpressionVar (mkName n))
+  Mono.IdenFunction n -> do
+    funInfo <- HashMap.lookupDefault impossible n <$> asks (^. Mono.infoFunctions)
+    let varName = case funInfo ^. Mono.functionInfoBuiltin of
+          Just builtin -> fromJust (builtinFunctionName builtin)
+          Nothing -> mkName n
+    return (ExpressionVar varName)
+  Mono.IdenConstructor n -> ExpressionVar <$> getConstructorCName n
   Mono.IdenVar n ->
     (^. bindingInfoExpr) . HashMap.lookupDefault impossible (n ^. Mono.nameText) <$> asks (^. patternBindings)
-  Mono.IdenAxiom n -> return (ExpressionVar (mkName n))
+  Mono.IdenAxiom n -> ExpressionVar <$> getAxiomCName n
 
-goApplication :: forall r. Members '[Reader PatternInfoTable, Reader Mono.InfoTable] r => Mono.Application -> Sem r Expression
+goApplication :: forall r. Members '[Reader PatternInfoTable, Builtins, Reader Mono.InfoTable] r => Mono.Application -> Sem r Expression
 goApplication a = do
   (iden, fArgs) <- f
 
@@ -340,27 +358,33 @@ goApplication a = do
                   args = reverse fArgs
                   patternArgs = take nPatterns args
                   funCall =
-                    if
-                        | null patternArgs -> idenExp
-                        | otherwise -> functionCall idenExp patternArgs
+                    (if null patternArgs then idenExp else functionCall idenExp patternArgs)
               return $ juvixFunctionCall callTyp funCall (drop nPatterns args)
           | otherwise -> do
               idenExp <- goIden iden
               return $ functionCall idenExp (reverse fArgs)
-    _ -> do
-      (idenType, _) <- getType iden
-      if
-          | (length fArgs < length (idenType ^. cFunArgTypes)) -> do
-              let name = mkName (Mono.getName iden)
-                  evalName = asEval (name <> "_" <> show (length fArgs))
-              return $ functionCall (ExpressionVar evalName) (reverse fArgs)
-          | otherwise -> do
-              idenExp <- goIden iden
-              return $ functionCall idenExp (reverse fArgs)
+    Mono.IdenConstructor n -> returnFunCall iden fArgs n
+    Mono.IdenAxiom n -> returnFunCall iden fArgs n
   where
     f :: Sem r (Mono.Iden, [Expression])
     f = unfoldApp a
 
+    returnFunCall :: Mono.Iden -> [Expression] -> Mono.Name -> Sem r Expression
+    returnFunCall iden fArgs name = do
+      (idenType, _) <- getType iden
+      ( if length fArgs < length (idenType ^. cFunArgTypes)
+          then
+            ( do
+                let evalName = asEval (mkName name <> "_" <> show (length fArgs))
+                return $ functionCall (ExpressionVar evalName) (reverse fArgs)
+            )
+          else
+            ( do
+                idenExp <- goIden iden
+                return $ functionCall idenExp (reverse fArgs)
+            )
+        )
+
     unfoldApp :: Mono.Application -> Sem r (Mono.Iden, [Expression])
     unfoldApp Mono.Application {..} = case _appLeft of
       Mono.ExpressionApplication x -> do
@@ -381,21 +405,23 @@ goAxiom ::
   Member (Reader Mono.CompileInfoTable) r =>
   Mono.AxiomDef ->
   Sem r [CCode]
-goAxiom a = do
-  backends <- lookupBackends (axiomName ^. Mono.nameId)
-  case firstJust getCode backends of
-    Nothing -> error ("C backend does not support this axiom:" <> show (axiomName ^. Mono.nameText))
-    Just defineBody ->
-      return
-        [ ExternalMacro
-            ( CppDefine
-                ( Define
-                    { _defineName = defineName,
-                      _defineBody = ExpressionVar defineBody
-                    }
+goAxiom a
+  | isJust (a ^. Mono.axiomBuiltin) = return []
+  | otherwise = do
+      backends <- lookupBackends (axiomName ^. Mono.nameId)
+      case firstJust getCode backends of
+        Nothing -> error ("C backend does not support this axiom:" <> show (axiomName ^. Mono.nameText))
+        Just defineBody ->
+          return
+            [ ExternalMacro
+                ( CppDefine
+                    ( Define
+                        { _defineName = defineName,
+                          _defineBody = ExpressionVar defineBody
+                        }
+                    )
                 )
-            )
-        ]
+            ]
   where
     axiomName :: Mono.Name
     axiomName = a ^. Mono.axiomName
@@ -443,15 +469,22 @@ mkInductiveTypeDef i =
     baseName :: Text
     baseName = mkName (i ^. Mono.inductiveName)
 
-goInductiveDef :: Mono.InductiveDef -> [CCode]
-goInductiveDef i =
-  [ ExternalDecl tagsType
-  ]
-    <> (i ^. Mono.inductiveConstructors >>= goInductiveConstructorDef)
-    <> [ExternalDecl inductiveDecl]
-    <> (i ^. Mono.inductiveConstructors >>= goInductiveConstructorNew i)
-    <> (ExternalFunc . isFunction <$> constructorNames)
-    <> (ExternalFunc . asFunction <$> constructorNames)
+goInductiveDef :: Members '[Reader Mono.InfoTable] r => Mono.InductiveDef -> Sem r [CCode]
+goInductiveDef i
+  | isJust (i ^. Mono.inductiveBuiltin) = return []
+  | otherwise = do
+      ctorDefs <- concatMapM goInductiveConstructorDef (i ^. Mono.inductiveConstructors)
+      ctorNews <- concatMapM (goInductiveConstructorNew i) (i ^. Mono.inductiveConstructors)
+      projections <- concatMapM (goProjections inductiveTypeDef) (i ^. Mono.inductiveConstructors)
+      return
+        ( [ExternalDecl tagsType]
+            <> ctorDefs
+            <> [ExternalDecl inductiveDecl]
+            <> ctorNews
+            <> (ExternalFunc . isFunction <$> constructorNames)
+            <> (ExternalFunc . asFunction <$> constructorNames)
+            <> projections
+        )
   where
     baseName :: Text
     baseName = mkName (i ^. Mono.inductiveName)
@@ -480,6 +513,9 @@ goInductiveDef i =
           _declInitializer = Nothing
         }
 
+    inductiveTypeDef :: DeclType
+    inductiveTypeDef = DeclTypeDefType (asTypeDef baseName)
+
     inductiveStruct :: DeclType
     inductiveStruct =
       DeclStructUnion
@@ -518,7 +554,7 @@ goInductiveDef i =
                 _funcIsPtr = False,
                 _funcQualifier = StaticInline,
                 _funcName = asIs ctorName,
-                _funcArgs = [ptrType (DeclTypeDefType (asTypeDef baseName)) funcArg]
+                _funcArgs = [ptrType inductiveTypeDef funcArg]
               },
           _funcBody =
             [ returnStatement
@@ -541,7 +577,7 @@ goInductiveDef i =
                 _funcIsPtr = False,
                 _funcQualifier = StaticInline,
                 _funcName = asCast ctorName,
-                _funcArgs = [ptrType (DeclTypeDefType (asTypeDef baseName)) funcArg]
+                _funcArgs = [ptrType inductiveTypeDef funcArg]
               },
           _funcBody =
             [ returnStatement
@@ -553,13 +589,15 @@ goInductiveDef i =
         funcArg = "a"
 
 goInductiveConstructorNew ::
+  forall r.
+  Members '[Reader Mono.InfoTable] r =>
   Mono.InductiveDef ->
   Mono.InductiveConstructorDef ->
-  [CCode]
+  Sem r [CCode]
 goInductiveConstructorNew i ctor = ctorNewFun
   where
-    ctorNewFun :: [CCode]
-    ctorNewFun = if null ctorParams then ctorNewNullary else ctorNewNary
+    ctorNewFun :: Sem r [CCode]
+    ctorNewFun = if null ctorParams then return ctorNewNullary else ctorNewNary
 
     baseName :: Text
     baseName = mkName (ctor ^. Mono.constructorName)
@@ -591,26 +629,29 @@ goInductiveConstructorNew i ctor = ctorNewFun
           )
       ]
 
-    ctorNewNary :: [CCode]
-    ctorNewNary =
-      [ ExternalFunc $
-          commonFunctionDeclr
-            baseName
-            ctorDecls
-            [ BodyDecl allocInductive,
-              BodyDecl ctorStructInit,
-              BodyDecl (commonInitDecl (dataInit tmpCtorStructName)),
-              BodyStatement assignPtr,
-              returnStatement (ExpressionVar tmpPtrName)
-            ]
-      ]
+    ctorNewNary :: Sem r [CCode]
+    ctorNewNary = do
+      ctorDecls' <- ctorDecls
+      ctorStructInit' <- ctorStructInit
+      return
+        [ ExternalFunc $
+            commonFunctionDeclr
+              baseName
+              ctorDecls'
+              [ BodyDecl allocInductive,
+                BodyDecl ctorStructInit',
+                BodyDecl (commonInitDecl (dataInit tmpCtorStructName)),
+                BodyStatement assignPtr,
+                returnStatement (ExpressionVar tmpPtrName)
+              ]
+        ]
       where
-        ctorDecls :: [Declaration]
+        ctorDecls :: Sem r [Declaration]
         ctorDecls = inductiveCtorArgs ctor
 
-        ctorInit :: [DesigInit]
+        ctorInit :: Sem r [DesigInit]
         -- TODO: _declName is never Nothing by construction, fix the types
-        ctorInit = map (f . fromJust . (^. declName)) ctorDecls
+        ctorInit = map (f . fromJust . (^. declName)) <$> ctorDecls
 
         f :: Text -> DesigInit
         f fieldName =
@@ -619,14 +660,16 @@ goInductiveConstructorNew i ctor = ctorNewFun
               _desigInitializer = ExprInitializer (ExpressionVar fieldName)
             }
 
-        ctorStructInit :: Declaration
-        ctorStructInit =
-          Declaration
-            { _declType = DeclTypeDefType (asTypeDef baseName),
-              _declIsPtr = False,
-              _declName = Just tmpCtorStructName,
-              _declInitializer = Just (DesignatorInitializer ctorInit)
-            }
+        ctorStructInit :: Sem r Declaration
+        ctorStructInit = do
+          ctorInit' <- ctorInit
+          return
+            Declaration
+              { _declType = DeclTypeDefType (asTypeDef baseName),
+                _declIsPtr = False,
+                _declName = Just tmpCtorStructName,
+                _declInitializer = Just (DesignatorInitializer ctorInit')
+              }
 
     commonFunctionDeclr :: Text -> [Declaration] -> [BodyItem] -> Function
     commonFunctionDeclr name args body =
@@ -709,20 +752,23 @@ goInductiveConstructorNew i ctor = ctorNewFun
             )
         )
 
-inductiveCtorArgs :: Mono.InductiveConstructorDef -> [Declaration]
-inductiveCtorArgs ctor = namedArgs asCtorArg (goType <$> ctorParams)
-  where
-    ctorParams :: [Mono.Type]
-    ctorParams = ctor ^. Mono.constructorParameters
+inductiveCtorParams :: Members '[Reader Mono.InfoTable] r => Mono.InductiveConstructorDef -> Sem r [CDeclType]
+inductiveCtorParams ctor = mapM goType (ctor ^. Mono.constructorParameters)
+
+inductiveCtorArgs :: Members '[Reader Mono.InfoTable] r => Mono.InductiveConstructorDef -> Sem r [Declaration]
+inductiveCtorArgs ctor = namedArgs asCtorArg <$> inductiveCtorParams ctor
 
 goInductiveConstructorDef ::
+  forall r.
+  Members '[Reader Mono.InfoTable] r =>
   Mono.InductiveConstructorDef ->
-  [CCode]
-goInductiveConstructorDef ctor =
-  [ExternalDecl ctorDecl]
+  Sem r [CCode]
+goInductiveConstructorDef ctor = do
+  d <- ctorDecl
+  return [ExternalDecl d]
   where
-    ctorDecl :: Declaration
-    ctorDecl = if null ctorParams then ctorBool else ctorStruct
+    ctorDecl :: Sem r Declaration
+    ctorDecl = if null ctorParams then return ctorBool else ctorStruct
 
     baseName :: Text
     baseName = mkName (ctor ^. Mono.constructorName)
@@ -733,15 +779,58 @@ goInductiveConstructorDef ctor =
     ctorBool :: Declaration
     ctorBool = typeDefWrap (asTypeDef baseName) BoolType
 
-    ctorStruct :: Declaration
-    ctorStruct = typeDefWrap (asTypeDef baseName) struct
+    ctorStruct :: Sem r Declaration
+    ctorStruct = typeDefWrap (asTypeDef baseName) <$> struct
 
-    struct :: DeclType
-    struct =
-      DeclStructUnion
-        ( StructUnion
-            { _structUnionTag = StructTag,
-              _structUnionName = Just (asStruct baseName),
-              _structMembers = Just (inductiveCtorArgs ctor)
-            }
+    struct :: Sem r DeclType
+    struct = do
+      args <- inductiveCtorArgs ctor
+      return
+        ( DeclStructUnion
+            ( StructUnion
+                { _structUnionTag = StructTag,
+                  _structUnionName = Just (asStruct baseName),
+                  _structMembers = Just args
+                }
+            )
         )
+
+goProjections ::
+  Members '[Reader Mono.InfoTable] r =>
+  DeclType ->
+  Mono.InductiveConstructorDef ->
+  Sem r [CCode]
+goProjections inductiveTypeDef ctor = do
+  params <- inductiveCtorParams ctor
+  return (ExternalFunc <$> zipWith projFunction [0 ..] params)
+  where
+    baseName :: Text
+    baseName = mkName (ctor ^. Mono.constructorName)
+
+    localName :: Text
+    localName = "a"
+
+    projFunction :: Int -> CDeclType -> Function
+    projFunction argIdx projTyp =
+      Function
+        { _funcSig =
+            FunctionSig
+              { _funcReturnType = projTyp ^. typeDeclType,
+                _funcIsPtr = projTyp ^. typeIsPtr,
+                _funcQualifier = StaticInline,
+                _funcName = asProj argIdx baseName,
+                _funcArgs = [namedDecl localName True inductiveTypeDef]
+              },
+          _funcBody =
+            [ BodyStatement
+                ( StatementReturn
+                    ( Just
+                        ( memberAccess
+                            Object
+                            (functionCall (ExpressionVar (asCast baseName)) [ExpressionVar localName])
+                            (asCtorArg (show argIdx))
+                        )
+                    )
+                )
+            ]
+        }
diff --git a/src/MiniJuvix/Translation/MonoJuvixToMiniC/Base.hs b/src/MiniJuvix/Translation/MonoJuvixToMiniC/Base.hs
index 0ec56f7345..381c773895 100644
--- a/src/MiniJuvix/Translation/MonoJuvixToMiniC/Base.hs
+++ b/src/MiniJuvix/Translation/MonoJuvixToMiniC/Base.hs
@@ -14,6 +14,7 @@ import MiniJuvix.Syntax.MicroJuvix.Language qualified as Micro
 import MiniJuvix.Syntax.MiniC.Language
 import MiniJuvix.Syntax.MonoJuvix.Language qualified as Mono
 import MiniJuvix.Translation.MicroJuvixToMonoJuvix qualified as Mono
+import MiniJuvix.Translation.MonoJuvixToMiniC.BuiltinTable
 import MiniJuvix.Translation.MonoJuvixToMiniC.CBuilder
 import MiniJuvix.Translation.MonoJuvixToMiniC.CNames
 import MiniJuvix.Translation.MonoJuvixToMiniC.Types
@@ -61,30 +62,36 @@ mkName n =
     idSuffix :: Text
     idSuffix = "_" <> show (n ^. Mono.nameId . Micro.unNameId)
 
-goType :: Mono.Type -> CDeclType
+goType :: forall r. Member (Reader Mono.InfoTable) r => Mono.Type -> Sem r CDeclType
 goType t = case t of
   Mono.TypeIden ti -> getMonoType ti
-  Mono.TypeFunction {} -> declFunctionPtrType
+  Mono.TypeFunction {} -> return declFunctionPtrType
   Mono.TypeUniverse {} -> unsupported "TypeUniverse"
   where
-    getMonoType :: Mono.TypeIden -> CDeclType
+    getMonoType :: Mono.TypeIden -> Sem r CDeclType
     getMonoType = \case
-      Mono.TypeIdenInductive mn ->
-        CDeclType
-          { _typeDeclType = DeclTypeDefType (asTypeDef (mkName mn)),
-            _typeIsPtr = True
-          }
-      Mono.TypeIdenAxiom mn ->
-        CDeclType
-          { _typeDeclType = DeclTypeDefType (mkName mn),
-            _typeIsPtr = False
-          }
-
-typeToFunType :: Mono.Type -> CFunType
-typeToFunType t =
-  let (_cFunArgTypes, _cFunReturnType) =
-        bimap (map goType) goType (unfoldFunType t)
-   in CFunType {..}
+      Mono.TypeIdenInductive mn -> do
+        (isPtr, name) <- getInductiveCName mn
+        return
+          ( CDeclType
+              { _typeDeclType = DeclTypeDefType name,
+                _typeIsPtr = isPtr
+              }
+          )
+      Mono.TypeIdenAxiom mn -> do
+        axiomName <- getAxiomCName mn
+        return
+          CDeclType
+            { _typeDeclType = DeclTypeDefType axiomName,
+              _typeIsPtr = False
+            }
+
+typeToFunType :: Member (Reader Mono.InfoTable) r => Mono.Type -> Sem r CFunType
+typeToFunType t = do
+  let (args, ret) = unfoldFunType t
+  _cFunArgTypes <- mapM goType args
+  _cFunReturnType <- goType ret
+  return CFunType {..}
 
 applyOnFunStatement ::
   forall a. Monoid a => (Mono.FunctionDef -> a) -> Mono.Statement -> a
@@ -94,18 +101,45 @@ applyOnFunStatement f = \case
   Mono.StatementAxiom {} -> mempty
   Mono.StatementInductive {} -> mempty
 
+getConstructorCName :: Members '[Reader Mono.InfoTable] r => Mono.Name -> Sem r Text
+getConstructorCName n = do
+  ctorInfo <- HashMap.lookupDefault impossible n <$> asks (^. Mono.infoConstructors)
+  return
+    ( case ctorInfo ^. Mono.constructorInfoBuiltin of
+        Just builtin -> fromJust (builtinConstructorName builtin)
+        Nothing -> mkName n
+    )
+
+getAxiomCName :: Members '[Reader Mono.InfoTable] r => Mono.Name -> Sem r Text
+getAxiomCName n = do
+  axiomInfo <- HashMap.lookupDefault impossible n <$> asks (^. Mono.infoAxioms)
+  return
+    ( case axiomInfo ^. Mono.axiomInfoBuiltin of
+        Just builtin -> fromJust (builtinAxiomName builtin)
+        Nothing -> mkName n
+    )
+
+getInductiveCName :: Members '[Reader Mono.InfoTable] r => Mono.Name -> Sem r (Bool, Text)
+getInductiveCName n = do
+  inductiveInfo <- HashMap.lookupDefault impossible n <$> asks (^. Mono.infoInductives)
+  return
+    ( case inductiveInfo ^. Mono.inductiveInfoBuiltin of
+        Just builtin -> (False, fromJust (builtinInductiveName builtin))
+        Nothing -> (True, asTypeDef (mkName n))
+    )
+
 buildPatternInfoTable :: forall r. Member (Reader Mono.InfoTable) r => [Mono.Type] -> Mono.FunctionClause -> Sem r PatternInfoTable
 buildPatternInfoTable argTyps Mono.FunctionClause {..} =
   PatternInfoTable . HashMap.fromList <$> patBindings
   where
-    funArgBindings :: [(Expression, CFunType)]
-    funArgBindings = bimap ExpressionVar typeToFunType <$> zip funArgs argTyps
+    funArgBindings :: Sem r [(Expression, CFunType)]
+    funArgBindings = mapM (bimapM (return . ExpressionVar) typeToFunType) (zip funArgs argTyps)
 
-    patArgBindings :: [(Mono.Pattern, (Expression, CFunType))]
-    patArgBindings = zip _clausePatterns funArgBindings
+    patArgBindings :: Sem r [(Mono.Pattern, (Expression, CFunType))]
+    patArgBindings = zip _clausePatterns <$> funArgBindings
 
     patBindings :: Sem r [(Text, BindingInfo)]
-    patBindings = concatMapM go patArgBindings
+    patBindings = patArgBindings >>= concatMapM go
 
     go :: (Mono.Pattern, (Expression, CFunType)) -> Sem r [(Text, BindingInfo)]
     go (p, (exp, typ)) = case p of
@@ -119,10 +153,10 @@ buildPatternInfoTable argTyps Mono.FunctionClause {..} =
     goConstructorApp :: Expression -> Mono.Name -> [Mono.Pattern] -> Sem r [(Text, BindingInfo)]
     goConstructorApp exp constructorName ps = do
       ctorInfo' <- ctorInfo
-      let ctorArgBindings :: [(Expression, CFunType)] =
-            bimap (memberAccess Object asConstructor) typeToFunType <$> zip ctorArgs ctorInfo'
-          patternCtorArgBindings :: [(Mono.Pattern, (Expression, CFunType))] = zip ps ctorArgBindings
-      concatMapM go patternCtorArgBindings
+      let ctorArgBindings :: Sem r [(Expression, CFunType)] =
+            mapM (bimapM asConstructor typeToFunType) (zip ctorArgs ctorInfo')
+          patternCtorArgBindings :: Sem r [(Mono.Pattern, (Expression, CFunType))] = zip ps <$> ctorArgBindings
+      patternCtorArgBindings >>= concatMapM go
       where
         ctorInfo :: Sem r [Mono.Type]
         ctorInfo = do
@@ -130,8 +164,10 @@ buildPatternInfoTable argTyps Mono.FunctionClause {..} =
           let fInfo = HashMap.lookupDefault impossible constructorName p'
           return $ fInfo ^. Mono.constructorInfoArgs
 
-        asConstructor :: Expression
-        asConstructor = functionCall (ExpressionVar (asCast (mkName constructorName))) [exp]
+        asConstructor :: Text -> Sem r Expression
+        asConstructor ctorArg = do
+          name <- getConstructorCName constructorName
+          return (functionCall (ExpressionVar (asProjName ctorArg name)) [exp])
 
 getType ::
   Members '[Reader Mono.InfoTable, Reader PatternInfoTable] r =>
@@ -140,22 +176,22 @@ getType ::
 getType = \case
   Mono.IdenFunction n -> do
     fInfo <- HashMap.lookupDefault impossible n <$> asks (^. Mono.infoFunctions)
-    return (typeToFunType (fInfo ^. Mono.functionInfoType), fInfo ^. Mono.functionInfoPatterns)
+    funTyp <- typeToFunType (fInfo ^. Mono.functionInfoType)
+    return (funTyp, fInfo ^. Mono.functionInfoPatterns)
   Mono.IdenConstructor n -> do
     fInfo <- HashMap.lookupDefault impossible n <$> asks (^. Mono.infoConstructors)
-    let argTypes = goType <$> (fInfo ^. Mono.constructorInfoArgs)
+    argTypes <- mapM goType (fInfo ^. Mono.constructorInfoArgs)
+    typ <- goType (Mono.TypeIden (Mono.TypeIdenInductive (fInfo ^. Mono.constructorInfoInductive)))
     return
       ( CFunType
           { _cFunArgTypes = argTypes,
-            _cFunReturnType =
-              goType
-                (Mono.TypeIden (Mono.TypeIdenInductive (fInfo ^. Mono.constructorInfoInductive)))
+            _cFunReturnType = typ
           },
         length argTypes
       )
   Mono.IdenAxiom n -> do
     fInfo <- HashMap.lookupDefault impossible n <$> asks (^. Mono.infoAxioms)
-    let t = typeToFunType (fInfo ^. Mono.axiomInfoType)
+    t <- typeToFunType (fInfo ^. Mono.axiomInfoType)
     return (t, length (t ^. cFunArgTypes))
   Mono.IdenVar n -> do
     t <- (^. bindingInfoType) . HashMap.lookupDefault impossible (n ^. Mono.nameText) <$> asks (^. patternBindings)
diff --git a/src/MiniJuvix/Translation/MonoJuvixToMiniC/BuiltinTable.hs b/src/MiniJuvix/Translation/MonoJuvixToMiniC/BuiltinTable.hs
new file mode 100644
index 0000000000..df4d286660
--- /dev/null
+++ b/src/MiniJuvix/Translation/MonoJuvixToMiniC/BuiltinTable.hs
@@ -0,0 +1,31 @@
+module MiniJuvix.Translation.MonoJuvixToMiniC.BuiltinTable where
+
+import MiniJuvix.Prelude
+import MiniJuvix.Syntax.Concrete.Builtins
+import MiniJuvix.Translation.MonoJuvixToMiniC.CNames
+
+builtinConstructorName :: BuiltinConstructor -> Maybe Text
+builtinConstructorName = \case
+  BuiltinNaturalZero -> Just zero
+  BuiltinNaturalSuc -> Just suc
+
+builtinInductiveName :: BuiltinInductive -> Maybe Text
+builtinInductiveName = \case
+  BuiltinNatural -> Just nat
+
+builtinAxiomName :: BuiltinAxiom -> Maybe Text
+builtinAxiomName = \case
+  BuiltinNaturalPrint -> Just printNat
+  BuiltinIO -> Just io
+  BuiltinIOSequence -> Just ioseq
+
+builtinFunctionName :: BuiltinFunction -> Maybe Text
+builtinFunctionName = \case
+  BuiltinNaturalPlus -> Just natplus
+
+builtinName :: BuiltinPrim -> Maybe Text
+builtinName = \case
+  BuiltinsInductive i -> builtinInductiveName i
+  BuiltinsConstructor i -> builtinConstructorName i
+  BuiltinsAxiom i -> builtinAxiomName i
+  BuiltinsFunction i -> builtinFunctionName i
diff --git a/src/MiniJuvix/Translation/MonoJuvixToMiniC/CBuilder.hs b/src/MiniJuvix/Translation/MonoJuvixToMiniC/CBuilder.hs
index c41554758d..d961a67767 100644
--- a/src/MiniJuvix/Translation/MonoJuvixToMiniC/CBuilder.hs
+++ b/src/MiniJuvix/Translation/MonoJuvixToMiniC/CBuilder.hs
@@ -6,20 +6,23 @@ import MiniJuvix.Syntax.MiniC.Language
 import MiniJuvix.Translation.MonoJuvixToMiniC.CNames
 
 namedArgs :: (Text -> Text) -> [CDeclType] -> [Declaration]
-namedArgs prefix = zipWith goTypeDecl argLabels
+namedArgs prefix = zipWith namedCDecl argLabels
   where
     argLabels :: [Text]
     argLabels = prefix . show <$> [0 :: Integer ..]
 
-goTypeDecl :: Text -> CDeclType -> Declaration
-goTypeDecl n CDeclType {..} =
+namedDecl :: Text -> Bool -> DeclType -> Declaration
+namedDecl n isPtr typ =
   Declaration
-    { _declType = _typeDeclType,
-      _declIsPtr = _typeIsPtr,
+    { _declType = typ,
+      _declIsPtr = isPtr,
       _declName = Just n,
       _declInitializer = Nothing
     }
 
+namedCDecl :: Text -> CDeclType -> Declaration
+namedCDecl n CDeclType {..} = namedDecl n _typeIsPtr _typeDeclType
+
 declFunctionType :: DeclType
 declFunctionType = DeclTypeDefType Str.minijuvixFunctionT
 
diff --git a/src/MiniJuvix/Translation/MonoJuvixToMiniC/CNames.hs b/src/MiniJuvix/Translation/MonoJuvixToMiniC/CNames.hs
index 36ded0c345..90c2967386 100644
--- a/src/MiniJuvix/Translation/MonoJuvixToMiniC/CNames.hs
+++ b/src/MiniJuvix/Translation/MonoJuvixToMiniC/CNames.hs
@@ -2,6 +2,33 @@ module MiniJuvix.Translation.MonoJuvixToMiniC.CNames where
 
 import MiniJuvix.Prelude
 
+primPrefix :: Text -> Text
+primPrefix = ("prim_" <>)
+
+zero :: Text
+zero = primPrefix "zero"
+
+suc :: Text
+suc = primPrefix "suc"
+
+printNat :: Text
+printNat = primPrefix "printNat"
+
+io :: Text
+io = primPrefix "io"
+
+nat :: Text
+nat = primPrefix "nat"
+
+int_ :: Text
+int_ = "int"
+
+ioseq :: Text
+ioseq = primPrefix "sequence"
+
+natplus :: Text
+natplus = primPrefix "natplus"
+
 funField :: Text
 funField = "fun"
 
@@ -23,6 +50,12 @@ asNullary n = n <> "_nullary"
 asCast :: Text -> Text
 asCast n = "as_" <> n
 
+asProjName :: Text -> Text -> Text
+asProjName argName n = "proj_" <> argName <> "_" <> n
+
+asProj :: Int -> Text -> Text
+asProj argIdx n = asProjName (asCtorArg (show argIdx)) n
+
 asIs :: Text -> Text
 asIs n = "is_" <> n
 
diff --git a/src/MiniJuvix/Translation/MonoJuvixToMiniC/Closure.hs b/src/MiniJuvix/Translation/MonoJuvixToMiniC/Closure.hs
index 0b78f92c97..cde67969f1 100644
--- a/src/MiniJuvix/Translation/MonoJuvixToMiniC/Closure.hs
+++ b/src/MiniJuvix/Translation/MonoJuvixToMiniC/Closure.hs
@@ -1,9 +1,10 @@
 module MiniJuvix.Translation.MonoJuvixToMiniC.Closure where
 
 import MiniJuvix.Prelude
+import MiniJuvix.Syntax.Concrete.Builtins (IsBuiltin (toBuiltinPrim))
 import MiniJuvix.Syntax.MiniC.Language
+import MiniJuvix.Syntax.MonoJuvix.InfoTable qualified as Mono
 import MiniJuvix.Syntax.MonoJuvix.Language qualified as Mono
-import MiniJuvix.Translation.MicroJuvixToMonoJuvix qualified as Mono
 import MiniJuvix.Translation.MonoJuvixToMiniC.Base
 
 genClosures ::
@@ -29,6 +30,13 @@ functionDefClosures ::
 functionDefClosures Mono.FunctionDef {..} =
   concatMapM (clauseClosures (fst (unfoldFunType _funDefType))) (toList _funDefClauses)
 
+lookupBuiltinIden :: Members '[Reader Mono.InfoTable] r => Mono.Iden -> Sem r (Maybe Mono.BuiltinPrim)
+lookupBuiltinIden = \case
+  Mono.IdenFunction f -> fmap toBuiltinPrim . (^. Mono.functionInfoBuiltin) <$> Mono.lookupFunction f
+  Mono.IdenConstructor c -> fmap toBuiltinPrim . (^. Mono.constructorInfoBuiltin) <$> Mono.lookupConstructor c
+  Mono.IdenAxiom a -> fmap toBuiltinPrim . (^. Mono.axiomInfoBuiltin) <$> Mono.lookupAxiom a
+  Mono.IdenVar {} -> return Nothing
+
 genClosureExpression ::
   forall r.
   Members '[Reader Mono.InfoTable, Reader PatternInfoTable] r =>
@@ -40,6 +48,7 @@ genClosureExpression funArgTyps = \case
     let rootFunMonoName = Mono.getName i
         rootFunNameId = rootFunMonoName ^. Mono.nameId
         rootFunName = mkName rootFunMonoName
+    builtin <- lookupBuiltinIden i
     case i of
       Mono.IdenVar {} -> return []
       _ -> do
@@ -52,6 +61,7 @@ genClosureExpression funArgTyps = \case
                   [ ClosureInfo
                       { _closureNameId = rootFunNameId,
                         _closureRootName = rootFunName,
+                        _closureBuiltin = builtin,
                         _closureMembers = [],
                         _closureFunType = t,
                         _closureCArity = patterns
@@ -66,15 +76,16 @@ genClosureExpression funArgTyps = \case
       let rootFunMonoName = Mono.getName f
           rootFunNameId = rootFunMonoName ^. Mono.nameId
           rootFunName = mkName rootFunMonoName
+      builtin <- lookupBuiltinIden f
       (fType, patterns) <- getType f
       closureArgs <- concatMapM (genClosureExpression funArgTyps) appArgs
-
       if
           | length appArgs < length (fType ^. cFunArgTypes) ->
               return
                 ( [ ClosureInfo
                       { _closureNameId = rootFunNameId,
                         _closureRootName = rootFunName,
+                        _closureBuiltin = builtin,
                         _closureMembers = take (length appArgs) (fType ^. cFunArgTypes),
                         _closureFunType = fType,
                         _closureCArity = patterns
@@ -169,7 +180,10 @@ genClosureApply c =
                     ),
                   BodyStatement . StatementReturn . Just $ juvixFunctionCall funType (ExpressionVar localFunName) (drop nPatterns args)
                 ]
-            | otherwise -> [BodyStatement . StatementReturn . Just $ functionCall (ExpressionVar (c ^. closureRootName)) args]
+            | otherwise ->
+                [ BodyStatement . StatementReturn . Just $
+                    functionCall (ExpressionVar (closureRootFunction c)) args
+                ]
       envArg :: BodyItem
       envArg =
         BodyDecl
diff --git a/src/MiniJuvix/Translation/MonoJuvixToMiniC/Types.hs b/src/MiniJuvix/Translation/MonoJuvixToMiniC/Types.hs
index 4ce198310d..1d128a5e99 100644
--- a/src/MiniJuvix/Translation/MonoJuvixToMiniC/Types.hs
+++ b/src/MiniJuvix/Translation/MonoJuvixToMiniC/Types.hs
@@ -3,6 +3,7 @@ module MiniJuvix.Translation.MonoJuvixToMiniC.Types where
 import MiniJuvix.Prelude
 import MiniJuvix.Syntax.MiniC.Language
 import MiniJuvix.Syntax.MonoJuvix.Language qualified as Mono
+import MiniJuvix.Translation.MonoJuvixToMiniC.BuiltinTable
 
 newtype MiniCResult = MiniCResult
   { _resultCCode :: Text
@@ -21,6 +22,7 @@ type CArity = Int
 data ClosureInfo = ClosureInfo
   { _closureNameId :: Mono.NameId,
     _closureRootName :: Text,
+    _closureBuiltin :: Maybe Mono.BuiltinPrim,
     _closureMembers :: [CDeclType],
     _closureFunType :: CFunType,
     _closureCArity :: CArity
@@ -34,3 +36,11 @@ makeLenses ''ClosureInfo
 makeLenses ''MiniCResult
 makeLenses ''PatternInfoTable
 makeLenses ''BindingInfo
+
+closureRootFunction :: ClosureInfo -> Text
+closureRootFunction c = case c ^. closureBuiltin of
+  Just b -> fromMaybe unsup (builtinName b)
+    where
+      unsup :: a
+      unsup = error ("unsupported builtin " <> show b)
+  Nothing -> c ^. closureRootName
diff --git a/src/MiniJuvix/Translation/MonoJuvixToMiniHaskell.hs b/src/MiniJuvix/Translation/MonoJuvixToMiniHaskell.hs
index aba8ab6d0b..9b0c54df53 100644
--- a/src/MiniJuvix/Translation/MonoJuvixToMiniHaskell.hs
+++ b/src/MiniJuvix/Translation/MonoJuvixToMiniHaskell.hs
@@ -77,7 +77,8 @@ goAxiomIden n = do
     getCode :: BackendItem -> Maybe Text
     getCode b =
       guard (BackendGhc == b ^. backendItemBackend)
-        $> b ^. backendItemCode
+        $> b
+        ^. backendItemCode
     lookupBackends ::
       Member (Reader Mono.CompileInfoTable) r =>
       NameId ->
diff --git a/src/MiniJuvix/Translation/ScopedToAbstract.hs b/src/MiniJuvix/Translation/ScopedToAbstract.hs
index 02ba043633..e63b85bbdf 100644
--- a/src/MiniJuvix/Translation/ScopedToAbstract.hs
+++ b/src/MiniJuvix/Translation/ScopedToAbstract.hs
@@ -4,10 +4,11 @@ module MiniJuvix.Translation.ScopedToAbstract
   )
 where
 
+import MiniJuvix.Builtins
+import MiniJuvix.Internal.NameIdGen
 import MiniJuvix.Prelude
 import MiniJuvix.Syntax.Abstract.AbstractResult
 import MiniJuvix.Syntax.Abstract.InfoTableBuilder
-import MiniJuvix.Syntax.Abstract.Language (FunctionDef (_funDefTypeSig))
 import MiniJuvix.Syntax.Abstract.Language qualified as Abstract
 import MiniJuvix.Syntax.Concrete.Language qualified as Concrete
 import MiniJuvix.Syntax.Concrete.Scoped.Error
@@ -18,7 +19,7 @@ import MiniJuvix.Syntax.Concrete.Scoped.Scoper qualified as Scoper
 unsupported :: Text -> a
 unsupported msg = error $ msg <> "Scoped to Abstract: not yet supported"
 
-entryAbstract :: Member (Error ScoperError) r => Scoper.ScoperResult -> Sem r AbstractResult
+entryAbstract :: Members '[Error ScoperError, Builtins, NameIdGen] r => Scoper.ScoperResult -> Sem r AbstractResult
 entryAbstract _resultScoper = do
   (_resultTable, _resultModules) <- runInfoTableBuilder (mapM goTopModule ms)
   return AbstractResult {..}
@@ -26,20 +27,20 @@ entryAbstract _resultScoper = do
     ms = _resultScoper ^. Scoper.resultModules
 
 goTopModule ::
-  Members '[InfoTableBuilder, Error ScoperError] r =>
+  Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen] r =>
   Module 'Scoped 'ModuleTop ->
   Sem r Abstract.TopModule
 goTopModule = goModule
 
 goLocalModule ::
-  Members '[InfoTableBuilder, Error ScoperError] r =>
+  Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen] r =>
   Module 'Scoped 'ModuleLocal ->
   Sem r Abstract.LocalModule
 goLocalModule = goModule
 
 goModule ::
   forall r t.
-  (Members '[InfoTableBuilder, Error ScoperError] r, SingI t) =>
+  (Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen] r, SingI t) =>
   Module 'Scoped t ->
   Sem r Abstract.Module
 goModule (Module n par b) = case par of
@@ -65,7 +66,7 @@ goSymbol s =
 
 goModuleBody ::
   forall r.
-  Members '[InfoTableBuilder, Error ScoperError] r =>
+  Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen] r =>
   [Statement 'Scoped] ->
   Sem r Abstract.ModuleBody
 goModuleBody ss' = do
@@ -102,7 +103,7 @@ goModuleBody ss' = do
 
 goStatement ::
   forall r.
-  Members '[InfoTableBuilder, Error ScoperError] r =>
+  Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen] r =>
   Indexed (Statement 'Scoped) ->
   Sem r (Maybe (Indexed Abstract.Statement))
 goStatement (Indexed idx s) =
@@ -122,7 +123,7 @@ goStatement (Indexed idx s) =
 
 goOpenModule ::
   forall r.
-  Members '[InfoTableBuilder, Error ScoperError] r =>
+  Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen] r =>
   OpenModule 'Scoped ->
   Sem r (Maybe Abstract.Statement)
 goOpenModule o
@@ -136,16 +137,19 @@ goOpenModule o
 
 goFunctionDef ::
   forall r.
-  Members '[InfoTableBuilder, Error ScoperError] r =>
+  Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen] r =>
   TypeSignature 'Scoped ->
   NonEmpty (FunctionClause 'Scoped) ->
   Sem r Abstract.FunctionDef
 goFunctionDef TypeSignature {..} clauses = do
   let _funDefName = goSymbol _sigName
       _funDefTerminating = _sigTerminating
+      _funDefBuiltin = _sigBuiltin
   _funDefClauses <- mapM goFunctionClause clauses
   _funDefTypeSig <- goExpression _sigType
-  registerFunction' Abstract.FunctionDef {..}
+  let fun = Abstract.FunctionDef {..}
+  whenJust _sigBuiltin (registerBuiltinFunction fun)
+  registerFunction' fun
 
 goFunctionClause ::
   Member (Error ScoperError) r =>
@@ -157,7 +161,8 @@ goFunctionClause FunctionClause {..} = do
   goWhereBlock _clauseWhere
   return
     Abstract.FunctionClause
-      { _clausePatterns = _clausePatterns',
+      { _clauseName = goSymbol _clauseOwnerFunction,
+        _clausePatterns = _clausePatterns',
         _clauseBody = _clauseBody'
       }
 
@@ -182,23 +187,50 @@ goInductiveParameter InductiveParameter {..} = do
         _paramUsage = UsageOmega
       }
 
+registerBuiltinInductive ::
+  Members '[InfoTableBuilder, Error ScoperError, Builtins] r =>
+  Abstract.InductiveDef ->
+  BuiltinInductive ->
+  Sem r ()
+registerBuiltinInductive d = \case
+  BuiltinNatural -> registerNaturalDef d
+
+registerBuiltinFunction ::
+  Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen] r =>
+  Abstract.FunctionDef ->
+  BuiltinFunction ->
+  Sem r ()
+registerBuiltinFunction d = \case
+  BuiltinNaturalPlus -> registerNaturalPlus d
+
+registerBuiltinAxiom ::
+  Members '[InfoTableBuilder, Error ScoperError, Builtins] r =>
+  Abstract.AxiomDef ->
+  BuiltinAxiom ->
+  Sem r ()
+registerBuiltinAxiom d = \case
+  BuiltinIO -> registerIO d
+  BuiltinIOSequence -> registerIOSequence d
+  BuiltinNaturalPrint -> registerNaturalPrint d
+
 goInductive ::
-  Members '[InfoTableBuilder, Error ScoperError] r =>
+  Members '[InfoTableBuilder, Builtins, Error ScoperError] r =>
   InductiveDef 'Scoped ->
   Sem r Abstract.InductiveDef
 goInductive InductiveDef {..} = do
   _inductiveParameters' <- mapM goInductiveParameter _inductiveParameters
   _inductiveType' <- mapM goExpression _inductiveType
   _inductiveConstructors' <- mapM goConstructorDef _inductiveConstructors
-  inductiveInfo <-
-    registerInductive
-      Abstract.InductiveDef
-        { _inductiveParameters = _inductiveParameters',
-          _inductiveName = goSymbol _inductiveName,
-          _inductiveType = _inductiveType',
-          _inductiveConstructors = _inductiveConstructors'
-        }
-
+  let indDef =
+        Abstract.InductiveDef
+          { _inductiveParameters = _inductiveParameters',
+            _inductiveBuiltin = _inductiveBuiltin,
+            _inductiveName = goSymbol _inductiveName,
+            _inductiveType = fromMaybe (Abstract.ExpressionUniverse smallUniverse) _inductiveType',
+            _inductiveConstructors = _inductiveConstructors'
+          }
+  whenJust _inductiveBuiltin (registerBuiltinInductive indDef)
+  inductiveInfo <- registerInductive indDef
   forM_ _inductiveConstructors' (registerConstructor inductiveInfo)
   return (inductiveInfo ^. inductiveInfoDef)
 
@@ -345,11 +377,14 @@ goPattern p = case p of
   PatternEmpty -> return Abstract.PatternEmpty
   PatternBraces b -> Abstract.PatternBraces <$> goPattern b
 
-goAxiom :: Members '[InfoTableBuilder, Error ScoperError] r => AxiomDef 'Scoped -> Sem r Abstract.AxiomDef
+goAxiom :: Members '[InfoTableBuilder, Error ScoperError, Builtins] r => AxiomDef 'Scoped -> Sem r Abstract.AxiomDef
 goAxiom a = do
   _axiomType' <- goExpression (a ^. axiomType)
-  registerAxiom'
-    Abstract.AxiomDef
-      { _axiomType = _axiomType',
-        _axiomName = goSymbol (a ^. axiomName)
-      }
+  let axiom =
+        Abstract.AxiomDef
+          { _axiomType = _axiomType',
+            _axiomBuiltin = a ^. axiomBuiltin,
+            _axiomName = goSymbol (a ^. axiomName)
+          }
+  whenJust (a ^. axiomBuiltin) (registerBuiltinAxiom axiom)
+  registerAxiom' axiom
diff --git a/src/MiniJuvix/Utils/Version.hs b/src/MiniJuvix/Utils/Version.hs
index 449cd42342..12e95a2cbb 100644
--- a/src/MiniJuvix/Utils/Version.hs
+++ b/src/MiniJuvix/Utils/Version.hs
@@ -56,16 +56,20 @@ infoVersionRepo :: IO (Doc Text)
 infoVersionRepo = do
   pNameTag <- progNameVersionTag
   return
-    ( PP.pretty pNameTag <> line
-        <> "Branch"
-        <> colon <+> PP.pretty branch
-        <> line
-        <> "Commit"
-        <> colon <+> PP.pretty commit
-        <> line
-        <> "Date"
-        <> colon <+> PP.pretty commitDate
+    ( PP.pretty pNameTag
         <> line
+        <> "Branch"
+        <> colon
+        <+> PP.pretty branch
+          <> line
+          <> "Commit"
+          <> colon
+        <+> PP.pretty commit
+          <> line
+          <> "Date"
+          <> colon
+        <+> PP.pretty commitDate
+          <> line
     )
 
 runDisplayVersion :: IO ()
diff --git a/test/BackendC/Base.hs b/test/BackendC/Base.hs
index bf13ce3c00..a950b77c9c 100644
--- a/test/BackendC/Base.hs
+++ b/test/BackendC/Base.hs
@@ -56,11 +56,16 @@ clangAssertion mainFile expectedFile stdinText step = do
   step "Compare expected and actual program output"
   assertEqDiff ("check: WASM output = " <> expectedFile) actualLibc expected
 
+builtinRuntime :: FilePath
+builtinRuntime = $(makeRelativeToProject "minic-runtime/builtins" >>= strToExp)
+
 standaloneArgs :: FilePath -> FilePath -> FilePath -> [String]
 standaloneArgs sysrootPath wasmOutputFile cOutputFile =
   [ "-nodefaultlibs",
     "-I",
     takeDirectory minicRuntime,
+    "-I",
+    builtinRuntime,
     "-Werror",
     "--target=wasm32-wasi",
     "--sysroot",
@@ -81,6 +86,8 @@ libcArgs sysrootPath wasmOutputFile cOutputFile =
   [ "-nodefaultlibs",
     "-I",
     takeDirectory minicRuntime,
+    "-I",
+    builtinRuntime,
     "-Werror",
     "-lc",
     "--target=wasm32-wasi",
diff --git a/test/BackendC/Positive.hs b/test/BackendC/Positive.hs
index 79e158cedb..f922782c6e 100644
--- a/test/BackendC/Positive.hs
+++ b/test/BackendC/Positive.hs
@@ -46,5 +46,6 @@ tests =
     PosTest "Closures with environment" "ClosureEnv",
     PosTest "SimpleFungibleTokenImplicit" "SimpleFungibleTokenImplicit",
     PosTest "Mutually recursive function" "MutuallyRecursive",
-    PosTest "Nested List type" "NestedList"
+    PosTest "Nested List type" "NestedList",
+    PosTest "Builtin types and functions" "Builtins"
   ]
diff --git a/tests/positive/MiniC/Builtins/Input.mjuvix b/tests/positive/MiniC/Builtins/Input.mjuvix
new file mode 100644
index 0000000000..186b0c875c
--- /dev/null
+++ b/tests/positive/MiniC/Builtins/Input.mjuvix
@@ -0,0 +1,31 @@
+module Input;
+
+builtin natural
+inductive ℕ {
+ zero : ℕ;
+ suc : ℕ → ℕ;
+};
+
+infixl 4 +;
+builtin natural-plus
++ : ℕ → ℕ → ℕ;
++ zero x ≔ x;
++ (suc a) b ≔ suc (a + b);
+
+mult : ℕ → ℕ → ℕ;
+mult zero _ ≔ zero;
+mult (suc n) m ≔ m + (mult n m);
+
+plusOne : ℕ → ℕ;
+plusOne ≔ suc;
+
+builtin IO axiom IO : Type;
+
+infixl 1 >>;
+builtin IO-sequence axiom >> : IO → IO → IO;
+builtin natural-print axiom printNat : ℕ → IO;
+
+main : IO;
+main ≔ printNat (mult 3 (2 + 2)) >> printNat 2;
+
+end;
diff --git a/tests/positive/MiniC/Builtins/expected.golden b/tests/positive/MiniC/Builtins/expected.golden
new file mode 100644
index 0000000000..533494143c
--- /dev/null
+++ b/tests/positive/MiniC/Builtins/expected.golden
@@ -0,0 +1,2 @@
+12
+2
diff --git a/tests/positive/MiniC/Builtins/minijuvix.yaml b/tests/positive/MiniC/Builtins/minijuvix.yaml
new file mode 100644
index 0000000000..e69de29bb2
diff --git a/tests/positive/MiniC/Lib/Data/Nat.mjuvix b/tests/positive/MiniC/Lib/Data/Nat.mjuvix
index 0f6d127057..89befe2846 100644
--- a/tests/positive/MiniC/Lib/Data/Nat.mjuvix
+++ b/tests/positive/MiniC/Lib/Data/Nat.mjuvix
@@ -9,9 +9,9 @@ inductive Nat {
 };
 
 foreign c {
-  void* natInd(int n, void* zero, minijuvix_function_t* suc) {
-    if (n <= 0) return zero;
-    return ((void* (*) (minijuvix_function_t*, void*))suc->fun)(suc, natInd(n - 1, zero, suc));
+  void* natInd(int n, void* zeroCtor, minijuvix_function_t* sucCtor) {
+    if (n <= 0) return zeroCtor;
+    return ((void* (*) (minijuvix_function_t*, void*))sucCtor->fun)(sucCtor, natInd(n - 1, zeroCtor, sucCtor));
   \}
 };