diff --git a/examples/milestone/ValidityPredicates/Anoma/Base.juvix b/examples/milestone/ValidityPredicates/Anoma/Base.juvix
index 8c0cf4e52c..5b745533df 100644
--- a/examples/milestone/ValidityPredicates/Anoma/Base.juvix
+++ b/examples/milestone/ValidityPredicates/Anoma/Base.juvix
@@ -36,7 +36,7 @@ open import Data.Int.Ops;
 import Stdlib.Data.String.Ord;
 
 from-int : Int → Maybe Int;
-from-int i ≔ if (i < 0) nothing (just i);
+from-int i ≔ if (i < Int_0) nothing (just i);
 
 from-string : String → Maybe String;
 from-string s ≔ if (s Stdlib.Data.String.Ord.== "") nothing (just s);
@@ -73,6 +73,6 @@ is-balance-key : String → String → Maybe String;
 is-balance-key token key ≔ from-string (isBalanceKey token key);
 
 unwrap-default : Maybe Int → Int;
-unwrap-default ≔ maybe 0 id;
+unwrap-default ≔ maybe Int_0 id;
 
 end;
diff --git a/examples/milestone/ValidityPredicates/Data/Int.juvix b/examples/milestone/ValidityPredicates/Data/Int.juvix
index 44ba6b2c62..58aadf08fd 100644
--- a/examples/milestone/ValidityPredicates/Data/Int.juvix
+++ b/examples/milestone/ValidityPredicates/Data/Int.juvix
@@ -6,4 +6,14 @@ compile Int {
   c ↦ "int";
 };
 
+axiom Int_0 : Int;
+compile Int_0 {
+  c ↦ "0";
+};
+
+axiom Int_1 : Int;
+compile Int_1 {
+  c ↦ "1";
+};
+
 end;
diff --git a/examples/milestone/ValidityPredicates/SimpleFungibleToken.juvix b/examples/milestone/ValidityPredicates/SimpleFungibleToken.juvix
index edb5ff6e6a..de82d6420b 100644
--- a/examples/milestone/ValidityPredicates/SimpleFungibleToken.juvix
+++ b/examples/milestone/ValidityPredicates/SimpleFungibleToken.juvix
@@ -9,7 +9,7 @@ import Data.Int.Ops;
 -- Misc
 
 pair-from-optionString : (String → Int × Bool) → Maybe String → Int × Bool;
-pair-from-optionString ≔ maybe (0 , false);
+pair-from-optionString ≔ maybe (Int_0 , false);
 
 -- Validity Predicate
 
@@ -19,7 +19,7 @@ change-from-key key ≔ unwrap-default (read-post key) Data.Int.Ops.- unwrap-def
 check-vp : List String → String → Int → String → Int × Bool;
 check-vp verifiers key change owner ≔
     if
-        (change-from-key key Data.Int.Ops.< 0)
+        (change-from-key key Data.Int.Ops.< Int_0)
         -- make sure the spender approved the transaction
         (change Data.Int.Ops.+ (change-from-key key), elem (Stdlib.Data.String.Ord.==) owner verifiers)
         (change Data.Int.Ops.+ (change-from-key key),  true);
@@ -29,16 +29,16 @@ check-keys token verifiers (change , is-success) key ≔
     if
         is-success
         (pair-from-optionString (check-vp verifiers key change) (is-balance-key token key))
-        (0 , false);
+        (Int_0 , false);
 
 check-result : Int × Bool → Bool;
-check-result (change , all-checked) ≔ (change Data.Int.Ops.== 0) && all-checked;
+check-result (change , all-checked) ≔ (change Data.Int.Ops.== Int_0) && all-checked;
 
 vp : String → List String → List String → Bool;
 vp token keys-changed verifiers ≔
     check-result
         (foldl
             (check-keys token verifiers)
-            (0 , true)
+            (Int_0 , true)
             keys-changed);
 end;
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal.hs
index 157f4b28b7..f220be3999 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal.hs
@@ -5,6 +5,7 @@ module Juvix.Compiler.Internal.Translation.FromInternal
 where
 
 import Data.HashMap.Strict qualified as HashMap
+import Juvix.Compiler.Builtins.Effect
 import Juvix.Compiler.Internal.Language
 import Juvix.Compiler.Internal.Translation.FromAbstract.Data.Context
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking qualified as ArityChecking
@@ -31,7 +32,7 @@ arityChecking res@InternalResult {..} =
     table = buildTable _resultModules
 
 typeChecking ::
-  Members '[Error JuvixError, NameIdGen] r =>
+  Members '[Error JuvixError, NameIdGen, Builtins] r =>
   ArityChecking.InternalArityResult ->
   Sem r InternalTypedResult
 typeChecking res@ArityChecking.InternalArityResult {..} =
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs
index 788ad9a351..d9a6436bfa 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs
@@ -100,7 +100,7 @@ guessArity ::
 guessArity = \case
   ExpressionHole {} -> return Nothing
   ExpressionFunction {} -> return (Just ArityUnit)
-  ExpressionLiteral {} -> return (Just arityLiteral)
+  ExpressionLiteral l -> return (Just (arityLiteral l))
   ExpressionApplication a -> appHelper a
   ExpressionIden i -> idenHelper i
   ExpressionUniverse {} -> return (Just arityUniverse)
@@ -133,18 +133,20 @@ guessArity = \case
           ExpressionUniverse {} -> return (Just arityUniverse)
           ExpressionApplication {} -> impossible
           ExpressionFunction {} -> return (Just ArityUnit)
-          ExpressionLiteral {} -> return (Just arityLiteral)
+          ExpressionLiteral l -> return (Just (arityLiteral l))
           ExpressionIden i -> idenHelper i
           ExpressionLambda {} -> lambda
 
 -- | The arity of all literals is assumed to be: {} -> 1
-arityLiteral :: Arity
-arityLiteral =
-  ArityFunction
-    FunctionArity
-      { _functionArityLeft = ParamImplicit,
-        _functionArityRight = ArityUnit
-      }
+arityLiteral :: LiteralLoc -> Arity
+arityLiteral (WithLoc _ l) = case l of
+  LitInteger {} -> ArityUnit
+  LitString {} ->
+    ArityFunction
+      FunctionArity
+        { _functionArityLeft = ParamImplicit,
+          _functionArityRight = ArityUnit
+        }
 
 arityUniverse :: Arity
 arityUniverse = ArityUnit
@@ -336,7 +338,7 @@ checkExpression hintArity expr = case expr of
       args' :: [(IsImplicit, Expression)] <- case fun of
         ExpressionHole {} -> mapM (secondM (checkExpression ArityUnknown)) args
         ExpressionIden i -> idenArity i >>= helper (getLoc i)
-        ExpressionLiteral l -> helper (getLoc l) arityLiteral
+        ExpressionLiteral l -> helper (getLoc l) (arityLiteral l)
         ExpressionUniverse l -> helper (getLoc l) arityUniverse
         ExpressionLambda {} -> lambda
         ExpressionFunction f ->
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs
index d3851f2ac8..cfbcb253a9 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs
@@ -5,6 +5,7 @@ module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Ch
 where
 
 import Data.HashMap.Strict qualified as HashMap
+import Juvix.Compiler.Builtins.Effect
 import Juvix.Compiler.Internal.Data.LocalVars
 import Juvix.Compiler.Internal.Extra
 import Juvix.Compiler.Internal.Pretty
@@ -22,7 +23,7 @@ registerConstructor ctr = do
   modify (HashMap.insert (ctr ^. inductiveConstructorName) ty)
 
 checkModule ::
-  Members '[Reader EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example] r =>
+  Members '[Reader EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins] r =>
   Module ->
   Sem r Module
 checkModule Module {..} = do
@@ -35,7 +36,7 @@ checkModule Module {..} = do
       }
 
 checkModuleBody ::
-  Members '[Reader EntryPoint, State NegativeTypeParameters, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example] r =>
+  Members '[Reader EntryPoint, State NegativeTypeParameters, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins] r =>
   ModuleBody ->
   Sem r ModuleBody
 checkModuleBody ModuleBody {..} = do
@@ -46,13 +47,13 @@ checkModuleBody ModuleBody {..} = do
       }
 
 checkInclude ::
-  Members '[Reader EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example] r =>
+  Members '[Reader EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins] r =>
   Include ->
   Sem r Include
 checkInclude = traverseOf includeModule checkModule
 
 checkStatement ::
-  Members '[Reader EntryPoint, State NegativeTypeParameters, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example] r =>
+  Members '[Reader EntryPoint, State NegativeTypeParameters, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins] r =>
   Statement ->
   Sem r Statement
 checkStatement s = case s of
@@ -66,7 +67,7 @@ checkStatement s = case s of
 
 checkInductiveDef ::
   forall r.
-  Members '[Reader EntryPoint, Reader InfoTable, Reader FunctionsTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, State NegativeTypeParameters, Output Example] r =>
+  Members '[Reader EntryPoint, Reader InfoTable, Reader FunctionsTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, State NegativeTypeParameters, Output Example, Builtins] r =>
   InductiveDef ->
   Sem r InductiveDef
 -- checkInductiveDef (InductiveDef name built params constrs pos) = runInferenceDef $ do
@@ -127,7 +128,7 @@ withEmptyVars :: Sem (Reader LocalVars : r) a -> Sem r a
 withEmptyVars = runReader emptyLocalVars
 
 checkFunctionDef ::
-  Members '[Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example] r =>
+  Members '[Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins] r =>
   FunctionDef ->
   Sem r FunctionDef
 checkFunctionDef FunctionDef {..} = do
@@ -145,7 +146,7 @@ checkFunctionDef FunctionDef {..} = do
   readerState @FunctionsTable (traverseOf funDefExamples (mapM checkExample) funDef)
 
 checkIsType ::
-  Members '[Reader InfoTable, Reader FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference] r =>
+  Members '[Reader InfoTable, Reader FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Builtins] r =>
   Interval ->
   Expression ->
   Sem r Expression
@@ -153,7 +154,7 @@ checkIsType = checkExpression . smallUniverseE
 
 checkFunctionDefType ::
   forall r.
-  Members '[Reader InfoTable, Reader FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference] r =>
+  Members '[Reader InfoTable, Reader FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Builtins] r =>
   Expression ->
   Sem r Expression
 checkFunctionDefType ty = do
@@ -165,7 +166,7 @@ checkFunctionDefType ty = do
     go h = freshMetavar h
 
 checkExample ::
-  Members '[Reader InfoTable, Reader FunctionsTable, Error TypeCheckerError, NameIdGen, Output Example, State TypesTable] r =>
+  Members '[Reader InfoTable, Reader FunctionsTable, Error TypeCheckerError, Builtins, NameIdGen, Output Example, State TypesTable] r =>
   Example ->
   Sem r Example
 checkExample e = do
@@ -174,7 +175,7 @@ checkExample e = do
   return e'
 
 checkExpression ::
-  Members '[Reader InfoTable, Reader FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference] r =>
+  Members '[Reader InfoTable, Reader FunctionsTable, Error TypeCheckerError, Builtins, NameIdGen, Reader LocalVars, Inference] r =>
   Expression ->
   Expression ->
   Sem r Expression
@@ -194,21 +195,13 @@ checkExpression expectedTy e = do
         )
 
 checkFunctionParameter ::
-  Members '[Reader InfoTable, Reader FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference] r =>
+  Members '[Reader InfoTable, Reader FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Builtins] r =>
   FunctionParameter ->
   Sem r FunctionParameter
 checkFunctionParameter (FunctionParameter mv i e) = do
   e' <- checkIsType (getLoc e) e
   return (FunctionParameter mv i e')
 
--- checkInductiveDef ::
---   Members '[Reader InfoTable, Error TypeCheckerError, State NegativeTypeParameters, Reader EntryPoint] r =>
---   InductiveDef ->
---   Sem r ()
--- checkInductiveDef ty@InductiveDef {..} = do
---   checkPositivity ty
---   mapM_ (checkConstructorDef ty) _inductiveConstructors
-
 checkConstructorDef ::
   Members
     '[ Reader EntryPoint,
@@ -251,7 +244,7 @@ checkConstructorReturnType indType ctor = do
     )
 
 inferExpression ::
-  Members '[Reader InfoTable, Reader FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference] r =>
+  Members '[Reader InfoTable, Reader FunctionsTable, Builtins, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference] r =>
   Expression ->
   Sem r Expression
 inferExpression = fmap (^. typedExpression) . inferExpression'
@@ -262,7 +255,7 @@ lookupVar v = HashMap.lookupDefault err v <$> asks (^. localTypes)
     err = error $ "internal error: could not find var " <> ppTrace v
 
 checkFunctionClauseBody ::
-  Members '[Reader InfoTable, Reader FunctionsTable, Error TypeCheckerError, NameIdGen, Inference] r =>
+  Members '[Reader InfoTable, Reader FunctionsTable, Error TypeCheckerError, NameIdGen, Builtins, Inference] r =>
   LocalVars ->
   Expression ->
   Expression ->
@@ -272,7 +265,7 @@ checkFunctionClauseBody locals expectedTy body =
 
 checkFunctionClause ::
   forall r.
-  Members '[Reader InfoTable, Reader FunctionsTable, Error TypeCheckerError, NameIdGen, Inference] r =>
+  Members '[Reader InfoTable, Reader FunctionsTable, Error TypeCheckerError, NameIdGen, Builtins, Inference] r =>
   Expression ->
   FunctionClause ->
   Sem r FunctionClause
@@ -457,9 +450,20 @@ freshHole l = do
   freshMetavar h
   return h
 
+literalType :: Members '[NameIdGen, Builtins] r => LiteralLoc -> Sem r TypedExpression
+literalType lit@(WithLoc i l) = case l of
+  LitInteger {} -> do
+    nat <- getBuiltinName i BuiltinNatural
+    return
+      TypedExpression
+        { _typedExpression = ExpressionLiteral lit,
+          _typedType = ExpressionIden (IdenInductive nat)
+        }
+  LitString {} -> literalMagicType lit
+
 -- | Returns {A : Expression} → A
-literalType :: Members '[NameIdGen] r => LiteralLoc -> Sem r TypedExpression
-literalType l = do
+literalMagicType :: Members '[NameIdGen] r => LiteralLoc -> Sem r TypedExpression
+literalMagicType l = do
   uid <- freshNameId
   let strA :: Text
       strA = "A"
@@ -491,7 +495,7 @@ literalType l = do
 
 inferExpression' ::
   forall r.
-  Members '[Reader InfoTable, Reader FunctionsTable, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference] r =>
+  Members '[Reader InfoTable, Reader FunctionsTable, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Builtins] r =>
   Expression ->
   Sem r TypedExpression
 inferExpression' e = case e of
diff --git a/src/Juvix/Compiler/Pipeline.hs b/src/Juvix/Compiler/Pipeline.hs
index 78de6176fa..4b64d9fdc0 100644
--- a/src/Juvix/Compiler/Pipeline.hs
+++ b/src/Juvix/Compiler/Pipeline.hs
@@ -152,7 +152,7 @@ pipelineAbstract ::
 pipelineAbstract = mapError (JuvixError @Scoper.ScoperError) . Abstract.fromConcrete
 
 pipelineInternalTyped ::
-  Members '[Files, NameIdGen, Error JuvixError] r =>
+  Members '[Files, NameIdGen, Error JuvixError, Builtins] r =>
   Internal.InternalArityResult ->
   Sem r Internal.InternalTypedResult
 pipelineInternalTyped =
diff --git a/tests/positive/FullExamples/MonoSimpleFungibleToken.juvix b/tests/positive/FullExamples/MonoSimpleFungibleToken.juvix
index fb7e1db11a..cd90612ed3 100644
--- a/tests/positive/FullExamples/MonoSimpleFungibleToken.juvix
+++ b/tests/positive/FullExamples/MonoSimpleFungibleToken.juvix
@@ -69,6 +69,11 @@ compile Int {
   ghc ↦ "Int";
 };
 
+axiom Int_0 : Int;
+compile Int_0 {
+  ghc ↦ "0";
+};
+
 axiom lt : Int → Int → BackendBool;
 compile lt {
   ghc ↦ "(<)";
@@ -156,7 +161,7 @@ if-optionInt true x _ ≔ x;
 if-optionInt false _ y ≔ y;
 
 from-int : Int → OptionInt;
-from-int i ≔ if-optionInt (i < 0) NothingInt (JustInt i);
+from-int i ≔ if-optionInt (i < Int_0) NothingInt (JustInt i);
 
 maybe-int : Int → OptionInt → Int;
 maybe-int d NothingInt ≔ d;
@@ -175,7 +180,7 @@ from-string : String → OptionString;
 from-string s ≔ if-optionString (s ==String "") NothingString (JustString s);
 
 pair-from-optionString : (String → PairIntBool) → OptionString → PairIntBool;
-pair-from-optionString _ NothingString ≔ MakePair 0 false;
+pair-from-optionString _ NothingString ≔ MakePair Int_0 false;
 pair-from-optionString f (JustString o) ≔ f o;
 
 --------------------------------------------------------------------------------
@@ -215,7 +220,7 @@ is-balance-key : String → String → OptionString;
 is-balance-key token key ≔ from-string (isBalanceKey token key);
 
 unwrap-default : OptionInt → Int;
-unwrap-default o ≔ maybe-int 0 o;
+unwrap-default o ≔ maybe-int Int_0 o;
 
 --------------------------------------------------------------------------------
 -- Validity Predicate
@@ -227,7 +232,7 @@ change-from-key key ≔ unwrap-default (read-post key) - unwrap-default (read-pr
 check-vp : ListString → String → Int → String → PairIntBool;
 check-vp verifiers key change owner ≔
     if-pairIntBool
-        (change-from-key key < 0)
+        (change-from-key key < Int_0)
         -- make sure the spender approved the transaction
         (MakePair (change + (change-from-key key)) (elem owner verifiers))
         (MakePair (change + (change-from-key key)) true);
@@ -237,17 +242,17 @@ check-keys token verifiers (MakePair change is-success) key ≔
     if-pairIntBool
         is-success
         (pair-from-optionString (check-vp verifiers key change) (is-balance-key token key))
-        (MakePair 0 false);
+        (MakePair Int_0 false);
 
 check-result : PairIntBool → Bool;
-check-result (MakePair change all-checked) ≔ (change ==Int 0) && all-checked;
+check-result (MakePair change all-checked) ≔ (change ==Int Int_0) && all-checked;
 
 vp : String → ListString → ListString → Bool;
 vp token keys-changed verifiers ≔
     check-result
         (foldl
             (check-keys token verifiers)
-            (MakePair 0 true)
+            (MakePair Int_0 true)
             keys-changed);
 
 --------------------------------------------------------------------------------
diff --git a/tests/positive/FullExamples/SimpleFungibleTokenImplicit.juvix b/tests/positive/FullExamples/SimpleFungibleTokenImplicit.juvix
index 8ca83c9e66..231046eb4e 100644
--- a/tests/positive/FullExamples/SimpleFungibleTokenImplicit.juvix
+++ b/tests/positive/FullExamples/SimpleFungibleTokenImplicit.juvix
@@ -81,6 +81,17 @@ compile Int {
   ghc ↦ "Int";
 };
 
+
+axiom Int_0 : Int;
+compile Int_0 {
+  c ↦ "0";
+};
+
+axiom Int_1 : Int;
+compile Int_1 {
+  c ↦ "1";
+};
+
 infix 4 <';
 axiom <' : Int → Int → BackendBool;
 compile <' {
@@ -168,7 +179,7 @@ inductive Maybe (A : Type) {
 };
 
 from-int : Int → Maybe Int;
-from-int i ≔ if (i < 0) nothing (just i);
+from-int i ≔ if (i < Int_0) nothing (just i);
 
 maybe : {A : Type} → {B : Type} → B → (A → B) → Maybe A → B;
 maybe b _ nothing ≔ b;
@@ -178,7 +189,7 @@ from-string : String → Maybe String;
 from-string s ≔ if (s ==String "") nothing (just s);
 
 pair-from-optionString : (String → Int × Bool) → Maybe String → Int × Bool;
-pair-from-optionString ≔ maybe (0 , false);
+pair-from-optionString ≔ maybe (Int_0 , false);
 
 --------------------------------------------------------------------------------
 -- Anoma
@@ -209,7 +220,7 @@ is-balance-key : String → String → Maybe String;
 is-balance-key token key ≔ from-string (isBalanceKey token key);
 
 unwrap-default : Maybe Int → Int;
-unwrap-default ≔ maybe 0 id;
+unwrap-default ≔ maybe Int_0 id;
 
 --------------------------------------------------------------------------------
 -- Validity Predicate
@@ -221,7 +232,7 @@ change-from-key key ≔ unwrap-default (read-post key) - unwrap-default (read-pr
 check-vp : List String → String → Int → String → Int × Bool;
 check-vp verifiers key change owner ≔
     if
-        (change-from-key key < 0)
+        (change-from-key key < Int_0)
         -- make sure the spender approved the transaction
         (change + (change-from-key key), elem (==String) owner verifiers)
         (change + (change-from-key key),  true);
@@ -231,17 +242,17 @@ check-keys token verifiers (change , is-success) key ≔
     if
         is-success
         (pair-from-optionString (check-vp verifiers key change) (is-balance-key token key))
-        (0 , false);
+        (Int_0 , false);
 
 check-result : Int × Bool → Bool;
-check-result (change , all-checked) ≔ (change ==Int 0) && all-checked;
+check-result (change , all-checked) ≔ (change ==Int Int_0) && all-checked;
 
 vp : String → List String → List String → Bool;
 vp token keys-changed verifiers ≔
     check-result
         (foldl
             (check-keys token verifiers)
-            (0 , true)
+            (Int_0 , true)
             keys-changed);
 
 --------------------------------------------------------------------------------
diff --git a/tests/positive/Internal/LiteralInt.juvix b/tests/positive/Internal/LiteralInt.juvix
index 4390dc297e..7d22b82c5f 100644
--- a/tests/positive/Internal/LiteralInt.juvix
+++ b/tests/positive/Internal/LiteralInt.juvix
@@ -1,4 +1,5 @@
 module LiteralInt;
+  open import Stdlib.Prelude;
   inductive A {
     a : A;
   };
@@ -7,6 +8,6 @@ module LiteralInt;
     b : B;
   };
 
-  f : A;
+  f : ℕ;
   f ≔ 1;
 end;
diff --git a/tests/positive/MiniC/AlwaysValidVP/Input.juvix b/tests/positive/MiniC/AlwaysValidVP/Input.juvix
index d5ab571108..f24b951aad 100644
--- a/tests/positive/MiniC/AlwaysValidVP/Input.juvix
+++ b/tests/positive/MiniC/AlwaysValidVP/Input.juvix
@@ -17,9 +17,19 @@ compile AnomaBool {
   c ↦ "uint64_t";
 };
 
+axiom AnomaBool_true : AnomaBool;
+compile AnomaBool_true {
+  c ↦ "1";
+};
+
+axiom AnomaBool_false : AnomaBool;
+compile AnomaBool_false {
+  c ↦ "0";
+};
+
 encodeBool : Bool → AnomaBool;
-encodeBool true ≔ 1;
-encodeBool false ≔ 0;
+encodeBool true ≔ AnomaBool_true;
+encodeBool false ≔ AnomaBool_false;
 
 --- The module entrypoint callable by wasm runtime
 _validate_tx : AnomaPtr → AnomaSize → AnomaPtr → AnomaSize → AnomaPtr → AnomaSize → AnomaPtr → AnomaSize → AnomaBool;
diff --git a/tests/positive/MiniC/Builtins/Input.juvix b/tests/positive/MiniC/Builtins/Input.juvix
index 186b0c875c..78f6f88832 100644
--- a/tests/positive/MiniC/Builtins/Input.juvix
+++ b/tests/positive/MiniC/Builtins/Input.juvix
@@ -19,6 +19,9 @@ mult (suc n) m ≔ m + (mult n m);
 plusOne : ℕ → ℕ;
 plusOne ≔ suc;
 
+someLiteral : _;
+someLiteral ≔ 123;
+
 builtin IO axiom IO : Type;
 
 infixl 1 >>;
diff --git a/tests/positive/MiniC/ClosureEnv/Input.juvix b/tests/positive/MiniC/ClosureEnv/Input.juvix
index 6adff67d40..92e3c476a9 100644
--- a/tests/positive/MiniC/ClosureEnv/Input.juvix
+++ b/tests/positive/MiniC/ClosureEnv/Input.juvix
@@ -4,11 +4,20 @@ open import Data.IO;
 open import Data.String;
 
 axiom Int : Type;
-
 compile Int {
   c ↦ "int";
 };
 
+axiom Int_0 : Int;
+compile Int_0 {
+  c ↦ "0";
+};
+
+axiom Int_1 : Int;
+compile Int_1 {
+  c ↦ "1";
+};
+
 axiom to-str : Int → String;
 
 compile to-str {
@@ -37,8 +46,8 @@ nplus zero n ≔ n;
 nplus (suc m) n ≔ suc (nplus m n);
 
 nplus-to-int : Nat → Int;
-nplus-to-int zero ≔ 0;
-nplus-to-int (suc n) ≔ plus 1 (nplus-to-int n);
+nplus-to-int zero ≔ Int_0;
+nplus-to-int (suc n) ≔ plus Int_1 (nplus-to-int n);
 
 nOne : Nat;
 nOne ≔ suc zero;
@@ -46,14 +55,17 @@ nOne ≔ suc zero;
 nplusOne : Nat → Nat → Nat;
 nplusOne n ≔ nplus nOne;
 
+plusOneInt : Int → Int;
+plusOneInt ≔ plus Int_1;
+
 one : Int;
-one ≔ 1;
+one ≔ Int_1;
 
 two : Int;
-two ≔ 2;
+two ≔ plusOneInt one;
 
 three : Int;
-three ≔ 3;
+three ≔ plusOneInt two;
 
 plusXIgnore2 : Int → Int → Int → Int → Int;
 plusXIgnore2 _ _ ≔ plus;
diff --git a/tests/positive/MiniC/ClosureNoEnv/Input.juvix b/tests/positive/MiniC/ClosureNoEnv/Input.juvix
index 230d357eba..09ad15d26c 100644
--- a/tests/positive/MiniC/ClosureNoEnv/Input.juvix
+++ b/tests/positive/MiniC/ClosureNoEnv/Input.juvix
@@ -4,11 +4,25 @@ open import Data.IO;
 open import Data.String;
 
 axiom Int : Type;
-
 compile Int {
   c ↦ "int";
 };
 
+axiom Int_0 : Int;
+compile Int_0 {
+  c ↦ "0";
+};
+
+axiom Int_1 : Int;
+compile Int_1 {
+  c ↦ "1";
+};
+
+axiom Int_2 : Int;
+compile Int_2 {
+  c ↦ "2";
+};
+
 axiom to-str : Int → String;
 
 compile to-str {
@@ -46,8 +60,8 @@ apply-nat2 : (Nat → Nat → Nat) → Nat → Nat → Nat;
 apply-nat2 f a b ≔ f a b;
 
 nat-to-int : Nat → Int;
-nat-to-int zero ≔ 0;
-nat-to-int (suc n) ≔ plus 1 (nat-to-int n);
+nat-to-int zero ≔ Int_0;
+nat-to-int (suc n) ≔ plus Int_1 (nat-to-int n);
 
 one : Nat;
 one ≔ suc zero;
@@ -60,7 +74,7 @@ two ≔ suc one;
 
 main : Action;
 main ≔ put-str "plus 1 2: "
-        >> put-str-ln (to-str (apply plus 1 2))
+        >> put-str-ln (to-str (apply plus Int_1 Int_2))
         >> put-str "suc one: "
         >> put-str-ln (to-str (nat-to-int (apply-nat suc one)))
         >> put-str "plus-nat 1 2: "
diff --git a/tests/positive/MiniC/HigherOrder/Input.juvix b/tests/positive/MiniC/HigherOrder/Input.juvix
index 89bb3cb3a9..8937247918 100644
--- a/tests/positive/MiniC/HigherOrder/Input.juvix
+++ b/tests/positive/MiniC/HigherOrder/Input.juvix
@@ -55,6 +55,16 @@ compile Int {
   c ↦ "int";
 };
 
+axiom Int_0 : Int;
+compile Int_0 {
+  c ↦ "0";
+};
+
+axiom Int_1 : Int;
+compile Int_1 {
+  c ↦ "1";
+};
+
 foreign c {
   int plus(int l, int r) {
     return l + r;
@@ -90,8 +100,8 @@ infixl 6 +;
 + (suc m) n ≔ suc (m + n);
 
 to-int : Nat → Int;
-to-int zero ≔ 0;
-to-int (suc n) ≔ 1 +int (to-int n);
+to-int zero ≔ Int_0;
+to-int (suc n) ≔ Int_1 +int (to-int n);
 
 nat-to-str : Nat → String;
 nat-to-str n ≔ to-str (to-int n);
diff --git a/tests/positive/MiniC/MultiModules/Data/Int.juvix b/tests/positive/MiniC/MultiModules/Data/Int.juvix
index 91becf5eda..1675b33978 100644
--- a/tests/positive/MiniC/MultiModules/Data/Int.juvix
+++ b/tests/positive/MiniC/MultiModules/Data/Int.juvix
@@ -7,6 +7,16 @@ compile Int {
   c ↦ "int";
 };
 
+axiom Int_0 : Int;
+compile Int_0 {
+  c ↦ "0";
+};
+
+axiom Int_1 : Int;
+compile Int_1 {
+  c ↦ "1";
+};
+
 axiom intToStr : Int → String;
 
 compile intToStr {
diff --git a/tests/positive/MiniC/MultiModules/Data/Nat.juvix b/tests/positive/MiniC/MultiModules/Data/Nat.juvix
index 2e2c601832..cb0e5ea1c4 100644
--- a/tests/positive/MiniC/MultiModules/Data/Nat.juvix
+++ b/tests/positive/MiniC/MultiModules/Data/Nat.juvix
@@ -22,8 +22,8 @@ compile natInd {
 };
 
 natToInt : Nat → Int;
-natToInt zero ≔ 0;
-natToInt (suc n) ≔ 1 + (natToInt n);
+natToInt zero ≔ Int_0;
+natToInt (suc n) ≔ Int_1 + (natToInt n);
 
 natToStr : Nat → String;
 natToStr n ≔ intToStr (natToInt n);
diff --git a/tests/positive/MiniC/MutuallyRecursive/Data/Int.juvix b/tests/positive/MiniC/MutuallyRecursive/Data/Int.juvix
index 91becf5eda..7d7774cebf 100644
--- a/tests/positive/MiniC/MutuallyRecursive/Data/Int.juvix
+++ b/tests/positive/MiniC/MutuallyRecursive/Data/Int.juvix
@@ -7,6 +7,27 @@ compile Int {
   c ↦ "int";
 };
 
+axiom Int_0 : Int;
+compile Int_0 {
+  c ↦ "0";
+};
+
+axiom Int_1 : Int;
+compile Int_1 {
+  c ↦ "1";
+};
+
+axiom Int_4 : Int;
+compile Int_4 {
+  c ↦ "4";
+};
+
+
+axiom Int_9 : Int;
+compile Int_9 {
+  c ↦ "9";
+};
+
 axiom intToStr : Int → String;
 
 compile intToStr {
diff --git a/tests/positive/MiniC/MutuallyRecursive/Data/Nat.juvix b/tests/positive/MiniC/MutuallyRecursive/Data/Nat.juvix
index 2e2c601832..cb0e5ea1c4 100644
--- a/tests/positive/MiniC/MutuallyRecursive/Data/Nat.juvix
+++ b/tests/positive/MiniC/MutuallyRecursive/Data/Nat.juvix
@@ -22,8 +22,8 @@ compile natInd {
 };
 
 natToInt : Nat → Int;
-natToInt zero ≔ 0;
-natToInt (suc n) ≔ 1 + (natToInt n);
+natToInt zero ≔ Int_0;
+natToInt (suc n) ≔ Int_1 + (natToInt n);
 
 natToStr : Nat → String;
 natToStr n ≔ intToStr (natToInt n);
diff --git a/tests/positive/MiniC/MutuallyRecursive/Input.juvix b/tests/positive/MiniC/MutuallyRecursive/Input.juvix
index 584beba6af..00fc608fa1 100644
--- a/tests/positive/MiniC/MutuallyRecursive/Input.juvix
+++ b/tests/positive/MiniC/MutuallyRecursive/Input.juvix
@@ -22,11 +22,11 @@ checkOdd : Int → String;
 checkOdd ≔ check odd;
 
 main : Action;
-main ≔ put-str "even 1: " >> put-str-ln (checkEven 1)
-        >> put-str "even 4: " >> put-str-ln (checkEven 4)
-        >> put-str "even 9: " >> put-str-ln (checkEven 9)
-        >> put-str "odd 1: " >> put-str-ln (checkOdd 1)
-        >> put-str "odd 4: " >> put-str-ln (checkOdd 4)
-        >> put-str "odd 9: " >> put-str-ln (checkOdd 9)
+main ≔ put-str "even 1: " >> put-str-ln (checkEven Int_1)
+        >> put-str "even 4: " >> put-str-ln (checkEven Int_4)
+        >> put-str "even 9: " >> put-str-ln (checkEven Int_9)
+        >> put-str "odd 1: " >> put-str-ln (checkOdd Int_1)
+        >> put-str "odd 4: " >> put-str-ln (checkOdd Int_4)
+        >> put-str "odd 9: " >> put-str-ln (checkOdd Int_9)
 
 end;
diff --git a/tests/positive/MiniC/Nat/Input.juvix b/tests/positive/MiniC/Nat/Input.juvix
index 65f20f578c..157a34e2be 100644
--- a/tests/positive/MiniC/Nat/Input.juvix
+++ b/tests/positive/MiniC/Nat/Input.juvix
@@ -68,12 +68,21 @@ bool-to-str false ≔ "False";
 --------------------------------------------------------------------------------
 
 axiom Int : Type;
-
 compile Int {
   ghc ↦ "Int";
   c ↦ "int";
 };
 
+axiom Int_0 : Int;
+compile Int_0 {
+  c ↦ "0";
+};
+
+axiom Int_1 : Int;
+compile Int_1 {
+  c ↦ "1";
+};
+
 foreign c {
   int plus(int l, int r) {
     return l + r;
@@ -121,8 +130,8 @@ infix 4 ==Nat;
 ==Nat _ _ ≔ false;
 
 to-int : Nat → Int;
-to-int zero ≔ 0;
-to-int (suc n) ≔ 1 +int (to-int n);
+to-int zero ≔ Int_0;
+to-int (suc n) ≔ Int_1 +int (to-int n);
 
 nat-to-str : Nat → String;
 nat-to-str n ≔ to-str (to-int n);
diff --git a/tests/positive/MiniC/PolymorphicTarget/Input.juvix b/tests/positive/MiniC/PolymorphicTarget/Input.juvix
index d8a8b2cf17..858a4eb1d6 100644
--- a/tests/positive/MiniC/PolymorphicTarget/Input.juvix
+++ b/tests/positive/MiniC/PolymorphicTarget/Input.juvix
@@ -20,7 +20,12 @@ compile Action {
   c ↦ "int";
 };
 
+axiom Int_0 : Action;
+compile Int_0 {
+  c ↦ "0";
+};
+
 main : Action;
-main := 0;
+main := Int_0;
 
 end;
diff --git a/tests/positive/MiniC/SimpleFungibleTokenImplicit/Input.juvix b/tests/positive/MiniC/SimpleFungibleTokenImplicit/Input.juvix
index 5ecd0dc659..138a6d7c41 100644
--- a/tests/positive/MiniC/SimpleFungibleTokenImplicit/Input.juvix
+++ b/tests/positive/MiniC/SimpleFungibleTokenImplicit/Input.juvix
@@ -98,10 +98,16 @@ id a ≔ a;
 --------------------------------------------------------------------------------
 
 axiom Int : Type;
+axiom Int_0 : Int;
+
 compile Int {
   c ↦ "int";
 };
 
+compile Int_0 {
+  c ↦ "0";
+};
+
 foreign c {
    bool lessThan(int l, int r) {
      return l < r;
@@ -130,6 +136,9 @@ infix 4 <;
 < : Int → Int → Bool;
 < i1 i2 ≔ from-backend-bool (i1 <' i2);
 
+isNegative : Int → Bool;
+isNegative n ≔ n < Int_0;
+
 axiom eqInt : Int → Int → BackendBool;
 compile eqInt {
   c ↦ "eqInt";
@@ -213,7 +222,7 @@ inductive Maybe (A : Type) {
 };
 
 from-int : Int → Maybe Int;
-from-int i ≔ if (i < 0) nothing (just i);
+from-int i ≔ if (isNegative i) nothing (just i);
 
 maybe : {A : Type} → {B : Type} → B → (A → B) → Maybe A → B;
 maybe b _ nothing ≔ b;
@@ -223,7 +232,7 @@ from-string : String → Maybe String;
 from-string s ≔ if (s ==String "") nothing (just s);
 
 pair-from-optionString : (String → Int × Bool) → Maybe String → Int × Bool;
-pair-from-optionString ≔ maybe (0 , false);
+pair-from-optionString ≔ maybe (Int_0 , false);
 
 --------------------------------------------------------------------------------
 -- Anoma
@@ -254,7 +263,7 @@ is-balance-key : String → String → Maybe String;
 is-balance-key token key ≔ from-string (isBalanceKey token key);
 
 unwrap-default : Maybe Int → Int;
-unwrap-default ≔ maybe 0 id;
+unwrap-default ≔ maybe Int_0 id;
 
 --------------------------------------------------------------------------------
 -- Validity Predicate
@@ -266,7 +275,7 @@ change-from-key key ≔ unwrap-default (read-post key) - unwrap-default (read-pr
 check-vp : List String → String → Int → String → Int × Bool;
 check-vp verifiers key change owner ≔
     if
-        (change-from-key key < 0)
+        (isNegative (change-from-key key))
         -- make sure the spender approved the transaction
         (change + (change-from-key key), elem (==String) owner verifiers)
         (change + (change-from-key key),  true);
@@ -276,17 +285,17 @@ check-keys token verifiers (change , is-success) key ≔
     if
         is-success
         (pair-from-optionString (check-vp verifiers key change) (is-balance-key token key))
-        (0 , false);
+        (Int_0 , false);
 
 check-result : Int × Bool → Bool;
-check-result (change , all-checked) ≔ (change ==Int 0) && all-checked;
+check-result (change , all-checked) ≔ (change ==Int Int_0) && all-checked;
 
 vp : String → List String → List String → Bool;
 vp token keys-changed verifiers ≔
     check-result
         (foldl
             (check-keys token verifiers)
-            (0 , true)
+            (Int_0 , true)
             keys-changed);
 
 --------------------------------------------------------------------------------