diff --git a/Apps/Sudoku.juvix b/Apps/Sudoku.juvix
index f1bf9ea..dbaf5ff 100644
--- a/Apps/Sudoku.juvix
+++ b/Apps/Sudoku.juvix
@@ -40,9 +40,6 @@ import Data.Map as Map;
 open Map using {Map};
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Int.Ord open;
-
-import Stdlib.Data.Nat.Ord as Nat;
 
 module Reward;
   staticData : ByteString := 0 :: nil;
@@ -60,7 +57,7 @@ end;
 
 --- Definitions related to the Sudoku ;Resource; in the application
 module Sudoku;
-  
+
   type Puzzle :=
     mkPuzzle {
       logicHash : LogicHash;
@@ -87,7 +84,7 @@ end;
     * The only squares that change between the previous and new solutinos
     are changes from zero (i.e unfilled) to non-zero (i.e filled).
  --}
-checkTransition (fromResource : Resource) (toResource : Resource) (reward : Resource)
+checkTransition {{Partial}} (fromResource : Resource) (toResource : Resource) (reward : Resource)
   : Bool :=
   let
     fromSolution : ByteString :=
@@ -99,7 +96,7 @@ checkTransition (fromResource : Resource) (toResource : Resource) (reward : Reso
     -- compared index-wise
     diff : List (Nat × Nat) :=
       filter (x, y in zip fromSolution toSolution)
-        x Nat./= y;
+        x /= y;
 
     -- Check that any solved squares in the toSolution are unsolved in the
     -- fromSolution
@@ -107,9 +104,9 @@ checkTransition (fromResource : Resource) (toResource : Resource) (reward : Reso
       all (consumedSquare, _ in diff)
         not (Sudoku.entryFilled? consumedSquare);
 
-  in length toSolution Nat.== length fromSolution
+  in length toSolution == length fromSolution
     && Sudoku.filledSquares toSolution
-      Nat.>= Sudoku.filledSquares fromSolution
+      >= Sudoku.filledSquares fromSolution
     && Sudoku.validGrid? (Sudoku.decode toSolution)
     && checkSolvedFromUnsolved
     && ofNat (length diff) == rewardQuantity;
@@ -131,7 +128,7 @@ vacuously valid.
 
 If the logic function part of a ;Resource; that is created by the partial
 transaction then it is valid. --}
-logicFunction : Sudoku.Puzzle -> LogicFunction
+logicFunction {{Partial}} : Sudoku.Puzzle -> LogicFunction
   | data kind tx :=
     let
       puzzleDenom : Denomination := Sudoku.denomination data;
@@ -156,16 +153,16 @@ logicFunction : Sudoku.Puzzle -> LogicFunction
 -- Definitions relating to the Dealer participant in the application
 module Dealer;
   {-- The logic function for the Sudoku dealer parital transaction.
-  
+
    Performs the following check:
-  
+
    If there is exactly one consumed ;Resource; representing a Sudoku puzzle then:
-  
+
    1. The solution matches the Dealer's solution.
-  
+
    If the partial transaction does not consume a Sudoku puzzle then it is
    vacuously valid.
-  
+
    If the logic function part of a ;Resource; that is created by the partial
    transaction then it is valid.
    --}
@@ -195,7 +192,7 @@ module Dealer;
   denomination (d : Sudoku.Puzzle) : Denomination
    := logicHash d :: staticData d;
 
-  mkResource (d : Sudoku.Puzzle) (n : Int) : Resource 
+  mkResource (d : Sudoku.Puzzle) (n : Int) : Resource
     := mkResource' (
     logicHash := logicHash d;
     staticData := staticData d;
@@ -213,7 +210,7 @@ dealer (puzzle : Sudoku.Puzzle)
         , Sudoku.mkResource puzzle initialBoard 1
     );
 
-logicFunctions (puzzle : Sudoku.Puzzle)
+logicFunctions {{Partial}} (puzzle : Sudoku.Puzzle)
  : Map LogicHash LogicFunction :=
   mkLogicFunctionMap
     ((Sudoku.Puzzle.logicHash puzzle
diff --git a/Apps/Sudoku/Extra.juvix b/Apps/Sudoku/Extra.juvix
index 5c3c1cc..ed3fe8f 100644
--- a/Apps/Sudoku/Extra.juvix
+++ b/Apps/Sudoku/Extra.juvix
@@ -2,8 +2,6 @@ module Apps.Sudoku.Extra;
 
 import Stdlib.Prelude open;
 
-import Stdlib.Data.Nat.Ord open;
-
 import Data.Set as Set;
 open Set using {Set};
 
diff --git a/Apps/Sudoku/Serializer.juvix b/Apps/Sudoku/Serializer.juvix
index 0ed8f3e..ad862cb 100644
--- a/Apps/Sudoku/Serializer.juvix
+++ b/Apps/Sudoku/Serializer.juvix
@@ -7,9 +7,6 @@ import Data.ByteString open;
 
 import Stdlib.Prelude open;
 
-import Stdlib.Data.Nat.Ord open;
-import Stdlib.Debug.Fail open;
-
 import Stdlib.Data.Nat.Ord as Nat;
 
 --- Encode a Sudoku ;Grid; to a ;ByteString;
@@ -29,7 +26,7 @@ floorSquareRoot : Nat -> Nat
 
 --- Partial function that computes a square root. If the input ;Nat; is not a
 --- square number then fail.
-checkSquareRoot (n : Nat) : Nat
+checkSquareRoot {{Partial}} (n : Nat) : Nat
 :=  let
     root : Nat := floorSquareRoot n;
   in if
@@ -38,24 +35,24 @@ checkSquareRoot (n : Nat) : Nat
     (fail "checkSquareRoot: not a square number");
 
 --- Decode a Sudoku ;Grid; from a ;ByteString;
-decode (bs : ByteString ) : Grid
+decode {{Partial}} (bs : ByteString ) : Grid
 :=  let
     gridWidth : Nat := checkSquareRoot (length bs);
-    
+
     subGridWidth : Nat := checkSquareRoot gridWidth;
 
     rows : List (List Nat) := chunksOf gridWidth bs;
-    
+
     split {A : Type} : List A -> List (List A) := chunksOf subGridWidth;
-    
+
     pack : List (List Nat) -> List (List (List (List Nat)))
       := split ∘ map split;
-    
-    unpack : List (List (List (List Nat))) -> List (List Nat) 
+
+    unpack : List (List (List (List Nat))) -> List (List Nat)
       := map flatten ∘ flatten;
     subGrids : List (List Nat) -> List (List Nat) := unpack ∘ map transpose ∘ pack;
 
-    decodeSubGrid : List Nat -> SubGrid 
+    decodeSubGrid : List Nat -> SubGrid
       := subGrid ∘ chunksOf subGridWidth;
   in grid
     (chunksOf subGridWidth (map decodeSubGrid (subGrids rows)));
diff --git a/Apps/Sudoku/Validator.juvix b/Apps/Sudoku/Validator.juvix
index a5072a3..7e0af65 100644
--- a/Apps/Sudoku/Validator.juvix
+++ b/Apps/Sudoku/Validator.juvix
@@ -3,8 +3,6 @@ module Apps.Sudoku.Validator;
 import Stdlib.Prelude open;
 import Data.ByteString open;
 
-import Stdlib.Data.Nat.Ord open;
-
 import Apps.Sudoku.Grid open public;
 import Apps.Sudoku.Extra open;
 
diff --git a/Apps/TwoPartyExchange.juvix b/Apps/TwoPartyExchange.juvix
index 04ce47a..cc87972 100644
--- a/Apps/TwoPartyExchange.juvix
+++ b/Apps/TwoPartyExchange.juvix
@@ -82,11 +82,10 @@ import Data.Map as Map;
 open Map using {Map};
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Int.Ord open;
 
 --- Definitions related to Alice's intent
 module AliceIntent;
-  
+
   logicFunction : LogicFunction
     | kind tx :=
       let
@@ -96,10 +95,10 @@ module AliceIntent;
         createdHashes : List LogicHash :=
           map Resource.logicHash createdRs;
       in isCreated kind
-        || (quantityOfDenom Dolphin.denomination createdRs == 1
-          && quantityOfDenom A.denomination createdRs == 1)
-        || quantityOfDenom Dolphin.denomination createdRs == 1
-        && quantityOfDenom B.denomination createdRs == 2;
+        || (quantityOfDenom Dolphin.denomination createdRs == ofNat 1
+          && quantityOfDenom A.denomination createdRs == ofNat 1)
+        || quantityOfDenom Dolphin.denomination createdRs == ofNat 1
+        && quantityOfDenom B.denomination createdRs == ofNat 2;
 
   --- This will be computed from the logic function
   logicHash : LogicHash := 1;
diff --git a/Simulator.juvix b/Simulator.juvix
index ec7158e..14faed7 100644
--- a/Simulator.juvix
+++ b/Simulator.juvix
@@ -7,13 +7,14 @@ import Simulator.PartialTx open public;
 import Simulator.Denomination open public;
 
 import Stdlib.Prelude open;
-import Stdlib.Debug.Fail open;
 import Data.ByteString open public;
 
 import Data.Map as Map;
 open Map using {Map};
 open Resource;
-validPartialTx (m : Map LogicHash LogicFunction) 
+
+validPartialTx {{Partial}}
+  (m : Map LogicHash LogicFunction)
   (ptx : PartialTx) : Bool :=
   let
     getLogicFn (kind : ResourceKind) (res : Resource)
@@ -42,8 +43,8 @@ balanceDelta (tx : PartialTx) : Balance :=
     (sumBalances (map mkBalance (consumedResources tx)))
     (sumBalances (map mkBalance (createdResources tx)));
 
-checkTransaction 
-  (m : Map LogicHash LogicFunction) 
+checkTransaction {{Partial}}
+  (m : Map LogicHash LogicFunction)
   (ptxs : List PartialTx) : Bool :=
   let
     allValid : Bool := all (validPartialTx m) ptxs;
diff --git a/Simulator/Balance.juvix b/Simulator/Balance.juvix
index d0e7e3b..fb71264 100644
--- a/Simulator/Balance.juvix
+++ b/Simulator/Balance.juvix
@@ -6,7 +6,6 @@ import Simulator.Resource open;
 import Simulator.Denomination open;
 
 import Data.Map as Map;
-import Stdlib.Data.Int as Int;
 import Stdlib.Data.Int.Ord as Int;
 
 type Balance :=
@@ -17,7 +16,7 @@ emptyBalance : Balance := balance nil;
 addBalance : Balance -> Balance -> Balance
   | (balance xs) (balance ys) :=
     balance
-      (Map.toList (Map.fromListWith (Int.+) (xs ++ ys)));
+      (Map.toList (Map.fromListWith (+) (xs ++ ys)));
 
 negateBalance : Balance -> Balance
   | (balance bs) := balance (map (b in bs) second neg b);
diff --git a/Simulator/Resource.juvix b/Simulator/Resource.juvix
index 0e238a5..2071e60 100644
--- a/Simulator/Resource.juvix
+++ b/Simulator/Resource.juvix
@@ -4,8 +4,6 @@ import Stdlib.Prelude open;
 import Data.ByteString open;
 import Simulator.Denomination open;
 
-import Stdlib.Data.Int as Int;
-
 --- A ;Resource; is an immutable object that represents part of an application's
 --- state.
 type Resource :=
@@ -34,8 +32,8 @@ resourcesForDenom (d : Denomination) (rs : List Resource)
 --- Aggregate the quantities associated with a denomination
 quantityOfDenom (d : Denomination) (rs : List Resource)
   : Int :=
-  for (acc := Int.ofNat 0) (r in resourcesForDenom d rs)
-    quantity r Int.+ acc;
+  for (acc := ofNat 0) (r in resourcesForDenom d rs)
+    quantity r + acc;
 
 --- Return true if the list is empty or the list has exactly 1 element and the predicate is satisfied
 zeroOrOneCheck : (Resource -> Bool) -> List Resource -> Bool
diff --git a/Test/AppsTest.juvix b/Test/AppsTest.juvix
index c4609af..cd3739f 100644
--- a/Test/AppsTest.juvix
+++ b/Test/AppsTest.juvix
@@ -16,7 +16,7 @@ open Sudoku hiding {logicFunctions};
 
 import Test.JuvixUnit open;
 
-twoPartyExchange : Test :=
+twoPartyExchange {{Partial}} : Test :=
   let
     txs : List PartialTx :=
       Alice.partialTransaction
@@ -29,8 +29,7 @@ twoPartyExchange : Test :=
       "expected two-party exchange transactions to validate"
       (checkTransaction TwoPartyExchange.logicFunctions txs));
 
-
-sudoku : Test :=
+sudoku {{Partial}} : Test :=
   let
     solution : ByteString :=
       1
@@ -51,12 +50,12 @@ sudoku : Test :=
         :: 3
         :: nil;
 
-    puzzleData : Sudoku.Puzzle := 
+    puzzleData : Sudoku.Puzzle :=
       Sudoku.mkPuzzle (logicHash := 3; solution := solution);
-    
+
     dealerPartialTx : PartialTx := dealer puzzleData (1 :: replicate 15 0);
 
-    alicePartialTx : PartialTx  := 
+    alicePartialTx : PartialTx  :=
       mkPartialTx (
         createdPair := Sudoku.mkResource puzzleData (1 :: 2 :: replicate 14 0) 1
             , Reward.mkResource 1;
@@ -66,10 +65,10 @@ sudoku : Test :=
 
     bobPartialTx : PartialTx :=
       mkPartialTx (
-        createdPair := 
+        createdPair :=
           Sudoku.mkResource puzzleData solution 0
             , Reward.mkResource 14;
-        consumedPair := 
+        consumedPair :=
           Sudoku.mkResource puzzleData (1 :: 2 :: replicate 14 0) 1
             , Dealer.mkResource puzzleData 1
           );
@@ -82,7 +81,7 @@ sudoku : Test :=
       "expected Sudoku solutions to validate"
       (checkTransaction (Sudoku.logicFunctions puzzleData) txs));
 
-emptyTest : Test :=
+emptyTest {{Partial}} : Test :=
   let
     emptyFunctions : Map LogicHash LogicFunction := Map.empty;
   in testCase
@@ -91,9 +90,10 @@ emptyTest : Test :=
       "expected transactions to validate"
       (checkTransaction emptyFunctions nil));
 
-tests : List Test := emptyTest :: 
-  twoPartyExchange :: 
-  sudoku :: 
+tests {{Partial}} : List Test := emptyTest ::
+  twoPartyExchange ::
+  sudoku ::
   nil;
 
-main : IO := runTestSuite (testSuite "Taiga simulator" tests);
+main : IO :=
+  runPartial λ {{{_}} := runTestSuite (testSuite "Taiga simulator" tests)};
diff --git a/Test/SudokuValidatorTest.juvix b/Test/SudokuValidatorTest.juvix
index 4ab3848..d7a4f5b 100644
--- a/Test/SudokuValidatorTest.juvix
+++ b/Test/SudokuValidatorTest.juvix
@@ -6,13 +6,13 @@ import Stdlib.Prelude open;
 
 import Test.JuvixUnit open;
 
-sudokuTests : List Test :=
+sudokuTests {{Partial}} : List Test :=
   let
     row1 : List SubGrid :=
       subGrid ((1 :: 2 :: nil) :: (3 :: 4 :: nil) :: nil)
         :: subGrid ((3 :: 4 :: nil) :: (1 :: 2 :: nil) :: nil)
         :: nil;
-    row2 : List SubGrid  :=
+    row2 : List SubGrid :=
       subGrid ((2 :: 3 :: nil) :: (4 :: 1 :: nil) :: nil)
         :: subGrid ((4 :: 1 :: nil) :: (2 :: 3 :: nil) :: nil)
         :: nil;
@@ -20,39 +20,38 @@ sudokuTests : List Test :=
     sudoku2InvalidShapeFull : Grid := grid (row1 :: nil);
     sudoku2DuplicatesFull : Grid := grid (row1 :: row1 :: nil);
     zeros : Nat -> List Nat
-    | zero := nil
-    | (suc n) := 0 :: zeros n;
+      | zero := nil
+      | (suc n) := 0 :: zeros n;
     zs : List Nat := zeros 2;
 
     emptyRow : List SubGrid :=
       subGrid (zs :: zs :: nil)
         :: subGrid (zs :: zs :: nil)
         :: nil;
-    
+
     sudoku2Empty : Grid := grid (emptyRow :: emptyRow :: nil);
-    
+
     sudoku2Partial : Grid := grid (row1 :: emptyRow :: nil);
 
-    decodedSol :
-      Grid :=
-        decode
-          (1
-            :: 2
-            :: 3
-            :: 4
-            :: 3
-            :: 4
-            :: 1
-            :: 2
-            :: 2
-            :: 3
-            :: 4
-            :: 1
-            :: 4
-            :: 1
-            :: 2
-            :: 3
-            :: nil);
+    decodedSol : Grid :=
+          decode
+            (1
+              :: 2
+              :: 3
+              :: 4
+              :: 3
+              :: 4
+              :: 1
+              :: 2
+              :: 2
+              :: 3
+              :: 4
+              :: 1
+              :: 4
+              :: 1
+              :: 2
+              :: 3
+              :: nil);
   in testCase
       "Basic 4x4 Sudoku is complete"
       (assertTrue
@@ -95,10 +94,11 @@ sudokuTests : List Test :=
         sudoku2Full
         (decode (encode sudoku2Full)))
     :: testCase
-      "4x4 paritally completed Sudoku is valid"
+      "4x4 partially completed Sudoku is valid"
       (assertTrue
         ("Expected grid to be valid\n" ++str prettyGrid decodedSol)
         (validGrid? decodedSol))
     :: nil;
 
-main : IO := runTestSuite (testSuite "Sudoku tests" sudokuTests);
+main : IO :=
+  runPartial λ {{{_}} := runTestSuite (testSuite "Sudoku tests" sudokuTests)};
diff --git a/juvix.yaml b/juvix.yaml
index 5448ab3..51ee87d 100644
--- a/juvix.yaml
+++ b/juvix.yaml
@@ -1,15 +1,15 @@
 dependencies:
 - git:
     url: https://github.com/anoma/juvix-stdlib
-    ref: 4facf14d9b2d06b81ce1be1882aa9050f768cb45
+    ref: 8493ff47a0c2fad4542c8e75f5736060ae7da0a4
     name: stdlib
 - git:
     url: https://github.com/anoma/juvix-test
-    ref: v0.6.1
+    ref: 3214a53b09a90fa77684a30d0fb2e14c202e99b5
     name: test
 - git:
     url: https://github.com/anoma/juvix-containers
-    ref: v0.7.0
+    ref: 7458d586a93caf9cc0ff678ef019c776c9f9b09f
     name: juvix-containers
 name: taiga-simulator
 version: 0.0.0