diff --git a/.github/workflows/telomare-ci.yml b/.github/workflows/telomare-ci.yml
index 293eac23..7320978a 100644
--- a/.github/workflows/telomare-ci.yml
+++ b/.github/workflows/telomare-ci.yml
@@ -8,8 +8,11 @@ jobs:
     runs-on: ubuntu-latest
     steps:
     - uses: actions/checkout@v4
+      with:
+        fetch-depth: 0
     - uses: cachix/install-nix-action@v25
       with:
+        install_url: https://releases.nixos.org/nix/nix-2.31.5/install
         nix_path: nixpkgs=channel:nixos-unstable
         extra_nix_config: |
           access-tokens = github.com=${{ secrets.GITHUB_TOKEN }}
@@ -46,8 +49,11 @@ jobs:
     steps:
       - name: Checkout telomare repository
         uses: actions/checkout@v4
+        with:
+          fetch-depth: 0
       - uses: cachix/install-nix-action@v25
         with:
+          install_url: https://releases.nixos.org/nix/nix-2.31.5/install
           extra_nix_config: |
             access-tokens = github.com=${{ secrets.GITHUB_TOKEN }}
       - uses: DeterminateSystems/magic-nix-cache-action@v2
@@ -72,8 +78,11 @@ jobs:
     steps:
       - name: Checkout telomare repository
         uses: actions/checkout@v4
+        with:
+          fetch-depth: 0
       - uses: cachix/install-nix-action@v25
         with:
+          install_url: https://releases.nixos.org/nix/nix-2.31.5/install
           extra_nix_config: |
             access-tokens = github.com=${{ secrets.GITHUB_TOKEN }}
       - uses: DeterminateSystems/magic-nix-cache-action@v2
@@ -103,14 +112,17 @@ jobs:
           repository: Stand-In-Language/stand-in-language
           token: ${{ secrets.API_TOKEN_GITHUB }}
           path: ./telomare
+          fetch-depth: 0
       - name: Checkout telomare site repository
         uses: actions/checkout@v4
         with:
           repository: Stand-In-Language/stand-in-language.github.io
           token: ${{ secrets.API_TOKEN_GITHUB }}
           path: ./stand-in-language.github.io
+          fetch-depth: 0
       - uses: cachix/install-nix-action@v25
         with:
+          install_url: https://releases.nixos.org/nix/nix-2.31.5/install
           extra_nix_config: |
             access-tokens = github.com=${{ secrets.GITHUB_TOKEN }}
       - uses: DeterminateSystems/magic-nix-cache-action@v2
diff --git a/Prelude.tel b/Prelude.tel
index 84d9c3f8..c54a782f 100644
--- a/Prelude.tel
+++ b/Prelude.tel
@@ -142,57 +142,45 @@ gcd = \a b ->
 
 lcm = \a b -> dDiv (dTimes a b) (gcd a b)
 
-Rational =
-  let wrapper = \h -> (
-        \n d -> if dEqual d 0
-                then abort "Denominator cannot be zero"
-                else
-                  let g   = gcd n d
-                      num = dDiv n g
-                      den = dDiv d g
-                  in (h, (num, den))
-      , \i -> if dEqual (left i) h
-              then right i
-              else abort "Not a Rational"
-      )
-  in wrapper (# wrapper)
-
-toRational = right Rational
-
-fromRational = left Rational
-
-rPlus = \a b ->
-  let n1 = left (right a)
-      d1 = right (right a)
-      n2 = left (right b)
-      d2 = right (right b)
-      num = dPlus (dTimes n1 d2) (dTimes n2 d1)
-      den = dTimes d1 d2
-  in fromRational num den
-
-rTimes = \a b ->
-  let n1 = left (right a)
-      d1 = right (right a)
-      n2 = left (right b)
-      d2 = right (right b)
-      num = dTimes n1 n2
-      den = dTimes d1 d2
-  in fromRational num den
-
-rMinus = \a b ->
-  let n1 = left (right a)
-      d1 = right (right a)
-      n2 = left (right b)
-      d2 = right (right b)
-      num = dMinus (dTimes n1 d2) (dTimes n2 d1)
-      den = dTimes d1 d2
-  in fromRational num den
-
-rDiv = \a b ->
-  let n1 = left (right a)
-      d1 = right (right a)
-      n2 = left (right b)
-      d2 = right (right b)
-      num = dTimes n1 d2
-      den = dTimes d1 n2
-  in fromRational num den
+[Rational, fromRational, toRational, rPlus, rTimes, rMinus, rDiv] = \h ->
+  [ \n d -> if dEqual d 0
+            then abort "Denominator cannot be zero"
+            else
+              let g   = gcd n d
+                  num = dDiv n g
+                  den = dDiv d g
+              in (h, (num, den))
+  , \i -> Rational i
+  , \a b ->
+      let n1 = left (right a)
+          d1 = right (right a)
+          n2 = left (right b)
+          d2 = right (right b)
+          num = dPlus (dTimes n1 d2) (dTimes n2 d1)
+          den = dTimes d1 d2
+      in fromRational num den
+  , \a b ->
+      let n1 = left (right a)
+          d1 = right (right a)
+          n2 = left (right b)
+          d2 = right (right b)
+          num = dTimes n1 n2
+          den = dTimes d1 d2
+      in fromRational num den
+  , \a b ->
+      let n1 = left (right a)
+          d1 = right (right a)
+          n2 = left (right b)
+          d2 = right (right b)
+          num = dMinus (dTimes n1 d2) (dTimes n2 d1)
+          den = dTimes d1 d2
+      in fromRational num den
+  , \a b ->
+      let n1 = left (right a)
+          d1 = right (right a)
+          n2 = left (right b)
+          d2 = right (right b)
+          num = dTimes n1 d2
+          den = dTimes d1 n2
+      in fromRational num den
+  ]
diff --git a/app/Evaluare.hs b/app/Evaluare.hs
index 2eb1a428..016ee265 100644
--- a/app/Evaluare.hs
+++ b/app/Evaluare.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE RecursiveDo #-}
+
 module Main where
 
 import Control.Comonad.Cofree (Cofree ((:<)))
@@ -164,16 +166,29 @@ nodify = removeExtraNumbers . fmap go . allNodes 0 where
 loadModules :: [String] -> IO [(String, [Either AnnotatedUPT (String, AnnotatedUPT)])]
 loadModules filenames = do
   filesStrings :: [String] <- mapM Strict.readFile filenames
-  case sequence $ parseModule <$> filesStrings of
+  case mapM parseModule filesStrings of
     Right p -> pure $ zip filesStrings p
     Left pe -> error pe
 
+mainWidgetInit
+  :: (forall t m.
+       ( MonadVtyApp t m
+       , HasImageWriter t m
+       , MonadNodeId m
+       , HasDisplayRegion t m
+       , HasFocusReader t m
+       , HasTheme t m
+       , HasInput t m
+       ) => Layout t (Focus t m) (Event t ()))
+  -> IO ()
+mainWidgetInit w = mainWidget (initManager_ w)
+
 main :: IO ()
 main = do
   modules :: [(String, [Either AnnotatedUPT (String, AnnotatedUPT)])] <- getArgs >>= loadModules
   let go :: Text -> IO ()
       go textErr =
-        mainWidget $ initManager_ $ do
+        mainWidgetInit $ do
           let cfg = def
                 { _textInputConfig_initialValue = TZ.fromText . T.pack . unlines $
                     [ "-- Example:"
@@ -185,14 +200,14 @@ main = do
               escOrCtrlcQuit :: (Monad m, HasInput t m, Reflex t) => m (Event t ())
               escOrCtrlcQuit = do
                 inp <- input
-                pure $ fforMaybe inp $ \case
+                pure . fforMaybe inp $ \case
                   V.EvKey (V.KChar 'c') [V.MCtrl] -> Just ()
                   V.EvKey V.KEsc []               -> Just ()
                   _                               -> Nothing
           getout <- escOrCtrlcQuit
           tile flex . box (pure roundedBoxStyle) . row $ do
             rec
-              eEitherIExpr :: Event t (Either String IExpr) <- grout flex $ col $ do
+              eEitherIExpr :: Event t (Either String IExpr) <- grout flex . col $ do
                 telomareTextInput :: TextInput t <- grout flex textBox
                 pure . updated $ TE.eval2IExpr modules . T.unpack <$> _textInput_value telomareTextInput
               grout (fixed 2) . col . text $ ""
diff --git a/app/Main.hs b/app/Main.hs
index 7396312f..bd93f28c 100644
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -2,10 +2,9 @@
 
 module Main where
 
+import Data.Maybe (mapMaybe)
 import qualified Options.Applicative as O
-import System.Directory (listDirectory)
-import System.FilePath (takeBaseName, takeExtension)
-import qualified System.IO.Strict as Strict
+import System.FilePath (takeBaseName)
 import Telomare.Eval (runMain)
 
 newtype TelomareOpts
@@ -16,15 +15,27 @@ telomareOpts :: O.Parser TelomareOpts
 telomareOpts = TelomareOpts
   <$> O.argument O.str (O.metavar "TELOMARE-FILE")
 
-getAllModules :: IO [(String, String)]
-getAllModules = do
-  allEntries <- listDirectory "."
-  let telFiles = filter (\f -> takeExtension f == ".tel") allEntries
-      readTelFile :: FilePath -> IO (String, String)
-      readTelFile file = do
-          content <- readFile file
-          return (takeBaseName file, content)
-  mapM readTelFile telFiles
+-- | Recursively load only the modules reachable from the entry file.
+getModulesFor :: String -> IO [(String, String)]
+getModulesFor entryModule = go [entryModule] []
+  where
+    go [] loaded = return loaded
+    go (m:queue) loaded
+      | m `elem` fmap fst loaded = go queue loaded
+      | otherwise = do
+          let filePath = m <> ".tel"
+          content <- readFile filePath
+          let imports = extractImports content
+          go (queue <> imports) ((m, content) : loaded)
+
+    extractImports :: String -> [String]
+    extractImports = mapMaybe parseImportLine . lines
+
+    parseImportLine :: String -> Maybe String
+    parseImportLine line = case words line of
+      ("import":"qualified":name:_) -> Just name
+      ("import":name:_)             -> Just name
+      _                             -> Nothing
 
 main :: IO ()
 main = do
@@ -32,5 +43,6 @@ main = do
         ( O.fullDesc
           <> O.progDesc "A simple but robust virtual machine" )
   topts <- O.execParser opts
-  allModules :: [(String, String)] <- getAllModules
-  runMain allModules . takeBaseName . telomareFile $ topts
+  let entryModule = takeBaseName (telomareFile topts)
+  allModules <- getModulesFor entryModule
+  runMain allModules entryModule
diff --git a/examples.tel b/examples.tel
index d7a2054f..f7042f38 100644
--- a/examples.tel
+++ b/examples.tel
@@ -1,35 +1,38 @@
+import Prelude
+
 -- File for small illustrative telomare programs and for testing
 
 -- Hello World example.
-aux = "Hello"
--- main = \input -> (aux, 0)
-main = \input -> ("Hello", 0)
+-- aux = "Hello"
+-- -- main = \input -> (aux, 0)
+-- main = \input -> ("Hello", 0)
 
--- -- refinement fail
+-- refinement fail
 -- main : (\x -> if x then "fail" else 0) = 1
+-- main : (\x -> assert 1 "fail") = 1
+-- main : (\x -> assert (not (left x)) "fail") = 1
+
+-- main : (\x -> assert (not x) "fail") = 1
 
 -- Ad hoc user defined types example:
 
--- MyInt = let wrapper = \h -> ( \i -> if not i
---                                     then abort "MyInt cannot be 0"
---                                     else  i
---                             , \i -> if dEqual (left i) h
---                                     then 0
---                                     else abort "Not a MyInt"
---                             )
---         in wrapper (# wrapper)
-
--- aux = \x -> if dEqual x 8 then "Success" else "Failure"
--- main = \i -> (aux ((left MyInt) 8), 0)
-
--- aux2 = [1,2,3]
-
--- something
--- main =
---   let toCase = (("a string", 99),(8,"pattern-match"))
---       caseTest =
---         case toCase of
---           (0,(8,2)) -> "Failure 1"
---           ("a string",(8,x)) -> concat [x, " failure 2"]
---           (("a string", 99),(8,x)) -> concat [x, " success with ints, strings and variables"]
---   in \input -> (caseTest, 0)
+-- Plain list assignments bind multiple names from a list-shaped value:
+-- [leftName, rightName] = ["left", "right"]
+-- [keep, drop] = \x -> [\_ -> x, \z -> z]
+
+[MyInt, mkMyInt, unMyInt] = \h ->
+  [ \i -> if not i
+          then abort "MyInt cannot be 0"
+          else (h, i)
+  , \(i : MyInt) -> i
+  ]
+
+aux = \x -> if dEqual x 8 then "Success" else "Failure"
+main = \i -> (aux (unMyInt (mkMyInt 8)), 0)
+
+-- User-defined type example used by the test suite:
+--   [Nat, toNat, nPlus, nMinus] = \h ->
+--     [ \x -> (h, x)
+--     , \(aa : Nat) (bb : Nat) -> (h, d2c aa succ bb)
+--     , \(aa : Nat) (bb : Nat) -> ...
+--     ]
diff --git a/flake.lock b/flake.lock
index b026d3ad..6b42f9da 100644
--- a/flake.lock
+++ b/flake.lock
@@ -3,11 +3,11 @@
     "flake-compat": {
       "flake": false,
       "locked": {
-        "lastModified": 1733328505,
-        "narHash": "sha256-NeCCThCEP3eCl2l/+27kNNK7QrwZB1IJCrXfrbv5oqU=",
+        "lastModified": 1767039857,
+        "narHash": "sha256-vNpUSpF5Nuw8xvDLj2KCwwksIbjua2LZCqhV1LNRDns=",
         "owner": "edolstra",
         "repo": "flake-compat",
-        "rev": "ff81ac966bb2cae68946d5ed5fc4994f96d0ffec",
+        "rev": "5edf11c44bc78a0d334f6334cdaf7d60d732daab",
         "type": "github"
       },
       "original": {
@@ -21,11 +21,11 @@
         "nixpkgs-lib": "nixpkgs-lib"
       },
       "locked": {
-        "lastModified": 1741352980,
-        "narHash": "sha256-+u2UunDA4Cl5Fci3m7S643HzKmIDAe+fiXrLqYsR2fs=",
+        "lastModified": 1778716662,
+        "narHash": "sha256-m1Yf0wZ8j1OHjTc2UwHwyQRSnNeSgLJOd7q5Y45hzi4=",
         "owner": "hercules-ci",
         "repo": "flake-parts",
-        "rev": "f4330d22f1c5d2ba72d3d22df5597d123fdb60a9",
+        "rev": "f7c1a2d347e4c52d5fb8d10cb4d94b5884e546fb",
         "type": "github"
       },
       "original": {
@@ -36,11 +36,11 @@
     },
     "haskell-flake": {
       "locked": {
-        "lastModified": 1741200839,
-        "narHash": "sha256-45psZ9Xd+50w9KrZmg1y5yH7MTm0J5pKWGD7GcRdPm0=",
+        "lastModified": 1779033714,
+        "narHash": "sha256-hhqI8XWucXQB5Yo6KwECkD2nldqNSd+ftfY3YoJT2/A=",
         "owner": "srid",
         "repo": "haskell-flake",
-        "rev": "b6508f818abb14a4df436378ff24e3e3afc9cbd0",
+        "rev": "375c8e3bf7c43a08eb74b60552de96f2561ade76",
         "type": "github"
       },
       "original": {
@@ -51,11 +51,11 @@
     },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1741380149,
-        "narHash": "sha256-KQiIzA4QoSqpXElTHhTgRhTrIP1/uz2nK46Pi1nGZ+M=",
+        "lastModified": 1779310261,
+        "narHash": "sha256-qYqCkHfJvq8Ha5PkVwlESuHGG326s29sJEdR19e2gsk=",
         "owner": "nixos",
         "repo": "nixpkgs",
-        "rev": "297f2c4266ed940780c8be68a82d85fb917c7d70",
+        "rev": "22b5577ab32f946edde57fb119c503e13634f2b4",
         "type": "github"
       },
       "original": {
@@ -66,11 +66,11 @@
     },
     "nixpkgs-lib": {
       "locked": {
-        "lastModified": 1740877520,
-        "narHash": "sha256-oiwv/ZK/2FhGxrCkQkB83i7GnWXPPLzoqFHpDD3uYpk=",
+        "lastModified": 1777168982,
+        "narHash": "sha256-GOkGPcboWE9BmGCRMLX3worL4EMnsnG8MyKmXNeYuhQ=",
         "owner": "nix-community",
         "repo": "nixpkgs.lib",
-        "rev": "147dee35aab2193b174e4c0868bd80ead5ce755c",
+        "rev": "f5901329dade4a6ea039af1433fb087bd9c1fe14",
         "type": "github"
       },
       "original": {
diff --git a/flake.nix b/flake.nix
index f6d2d4c8..d427f261 100644
--- a/flake.nix
+++ b/flake.nix
@@ -44,24 +44,11 @@
           #     jailbreak = true;
           #   };
           # };
-	  settings = {
-	    telomare = {
-		extraBuildDepends = with pkgs; [
-		  # Node.js and npm for Claude Code
-		  #nodejs_20
-		  nodejs_22
-		  nodePackages.npm
-		];
-	    };
-	  };
           devShell = {
             enable = true;
             tools = hp: {
               inherit (hp) cabal-install haskell-language-server;
-            } // {
-	      inherit (pkgs) nodejs_22;
-	      inherit (pkgs.nodePackages) npm;
-	    };
+            };
           };
       };
 
@@ -83,6 +70,128 @@
         type = "app";
         program = "${self.packages.${system}.telomare}/bin/telomare-lsp";
       };
+      apps.format-lint = {
+        type = "app";
+        program = "${pkgs.writeShellApplication {
+          name = "telomare-format-lint-check";
+          runtimeInputs = [
+            pkgs.diffutils
+            pkgs.git
+            pkgs.haskellPackages.hlint
+            pkgs.haskellPackages.stylish-haskell
+          ];
+          text = ''
+            mapfile -t hs_files < <(git ls-files '*.hs')
+            tmp_dir="$(mktemp -d)"
+            trap 'rm -rf "$tmp_dir"' EXIT
+
+            format_status=0
+            if [ "''${#hs_files[@]}" -gt 0 ]; then
+              for hs_file in "''${hs_files[@]}"; do
+                formatted_file="$tmp_dir/$(basename "$hs_file")"
+                stylish-haskell "$hs_file" > "$formatted_file"
+
+                if ! cmp -s "$hs_file" "$formatted_file"; then
+                  printf '%s needs formatting. Suggested diff:\n' "$hs_file"
+                  diff -u "$hs_file" "$formatted_file" || true
+                  format_status=1
+                fi
+              done
+            fi
+
+            if [ "$format_status" -ne 0 ]; then
+              exit "$format_status"
+            fi
+
+            hlint .
+
+            printf 'Formatting and linting are OK\n'
+          '';
+        }}/bin/telomare-format-lint-check";
+      };
+      apps.push-cachix = {
+        type = "app";
+        program = "${pkgs.writeShellApplication {
+          name = "telomare-push-cachix";
+          runtimeInputs = [
+            pkgs.cachix
+            pkgs.jq
+            pkgs.nixVersions.nix_2_31
+          ];
+          text = ''
+            cache_name=telomare
+            tmp_dir="$(mktemp -d)"
+            trap 'rm -rf "$tmp_dir"' EXIT
+
+            direct_paths="$tmp_dir/direct-paths"
+            closure_paths="$tmp_dir/closure-paths"
+            key_paths="$tmp_dir/key-paths"
+            : > "$direct_paths"
+            : > "$key_paths"
+
+            build_target() {
+              local target="$1"
+              local output_path
+              printf 'Building %s\n' "$target"
+              output_path="$(nix build --no-link --print-out-paths "$target")"
+              printf '%s\n' "$output_path" >> "$direct_paths"
+              printf '%s\n' "$output_path" >> "$key_paths"
+            }
+
+            build_target ".#packages.${system}.default"
+            build_target ".#checks.${system}.default"
+            build_target ".#devShells.${system}.default"
+
+            printf 'Building nix develop environment closure\n'
+            dev_env_profile="$tmp_dir/dev-env-profile"
+            nix print-dev-env --profile "$dev_env_profile" ".#devShells.${system}.default" >/dev/null
+            dev_env_path="$(nix path-info "$dev_env_profile")"
+            printf '%s\n' "$dev_env_path" >> "$direct_paths"
+            printf '%s\n' "$dev_env_path" >> "$key_paths"
+
+            printf 'Building legacy default.nix with nix-build\n'
+            legacy_build_path="$(nix-build --no-out-link)"
+            printf '%s\n' "$legacy_build_path" >> "$direct_paths"
+            printf '%s\n' "$legacy_build_path" >> "$key_paths"
+
+            printf 'Building legacy shell.nix closure with nix-store\n'
+            legacy_shell_drv="$(nix-instantiate shell.nix)"
+            legacy_shell_path="$(nix-store --realise "$legacy_shell_drv")"
+            printf '%s\n' "$legacy_shell_path" >> "$direct_paths"
+            printf '%s\n' "$legacy_shell_path" >> "$key_paths"
+            nix-store --query --requisites --include-outputs "$legacy_shell_drv" >> "$direct_paths"
+
+            printf 'Archiving flake source and inputs\n'
+            nix flake archive --json \
+              | jq -r '.. | objects | .path? // empty' \
+              >> "$direct_paths"
+
+            for app_name in default repl evaluare lsp format-lint; do
+              app_program="$(nix eval --raw ".#apps.${system}.$app_name.program")"
+              if [[ "$app_program" =~ ^(/nix/store/[^/]+) ]]; then
+                printf '%s\n' "''${BASH_REMATCH[1]}" >> "$direct_paths"
+              fi
+            done
+
+            sort -u "$direct_paths" \
+              | xargs nix path-info --recursive \
+              | sort -u \
+              > "$closure_paths"
+
+            path_count="$(wc -l < "$closure_paths")"
+            printf 'Pushing %s store paths to Cachix cache %s\n' "$path_count" "$cache_name"
+            cachix push "$cache_name" < "$closure_paths"
+
+            printf 'Verifying key paths in Cachix cache %s\n' "$cache_name"
+            while IFS= read -r key_path; do
+              printf 'Verifying %s\n' "$key_path"
+              nix path-info --store "https://$cache_name.cachix.org" "$key_path" >/dev/null
+            done < "$key_paths"
+
+            printf 'Cachix push completed for cache %s\n' "$cache_name"
+          '';
+        }}/bin/telomare-push-cachix";
+      };
 
       checks = self'.packages;
     };
diff --git a/src/PrettyPrint.hs b/src/PrettyPrint.hs
index 256ea57c..f1d3c7e1 100644
--- a/src/PrettyPrint.hs
+++ b/src/PrettyPrint.hs
@@ -348,61 +348,56 @@ newtype MultiLineShowUPT = MultiLineShowUPT UnprocessedParsedTerm
 instance Show MultiLineShowUPT where
   show (MultiLineShowUPT upt) = cata alg upt where
     alg :: Base UnprocessedParsedTerm String -> String
+    ind = indentSansFirstLine 2
     alg = \case
       IntUPF i -> "IntUP " <> show i
       VarUPF str -> "VarUP " <> str
-      StringUPF str -> "StringUP" <> str
-      PairUPF x y -> "PairUP" <> "\n" <>
-                        "  (" <> indentSansFirstLine 3 x <> ")\n" <>
-                        "  (" <> indentSansFirstLine 3 y <> ")"
-      (ITEUPF x y z) -> "ITEUP" <> "\n" <>
-                        "  (" <> indentSansFirstLine 3 x <> ")\n" <>
-                        "  (" <> indentSansFirstLine 3 x <> ")\n" <>
-                        "  (" <> indentSansFirstLine 3 z <> ")"
-      (AppUPF x y) -> "AppUP" <> "\n" <>
-                        "  (" <> indentSansFirstLine 3 x <> ")\n" <>
-                        "  (" <> indentSansFirstLine 3 y <> ")"
+      StringUPF str -> "StringUP " <> show str
+      PairUPF x y -> "PairUP\n" <>
+                        "  " <> ind x <> "\n" <>
+                        "  " <> ind y
+      (ITEUPF x y z) -> "ITEUP\n" <>
+                        "  " <> ind x <> "\n" <>
+                        "  " <> ind y <> "\n" <>
+                        "  " <> ind z
+      (AppUPF x y) -> "AppUP\n" <>
+                        "  " <> ind x <> "\n" <>
+                        "  " <> ind y
       (LamUPF str y) -> "LamUP " <> str <> "\n" <>
-                        "  (" <> indentSansFirstLine 3 y <> ")"
+                        "  " <> ind y
       (ChurchUPF x) -> "ChurchUP " <> show x
-      (LeftUPF x) -> "LeftUP \n" <>
-                       "  (" <> indentSansFirstLine 3 x <> ")"
-      (RightUPF x) -> "RightUP \n" <>
-                        "  (" <> indentSansFirstLine 3 x <> ")"
-      (TraceUPF x) -> "TraceUP \n" <>
-                        "  (" <> indentSansFirstLine 3 x <> ")"
-      (UnsizedRecursionUPF x y z) -> "UnsizedRecursionUP" <> "\n" <>
-                        "  (" <> indentSansFirstLine 3 x <> ")\n" <>
-                        "  (" <> indentSansFirstLine 3 x <> ")\n" <>
-                        "  (" <> indentSansFirstLine 3 z <> ")"
-      (HashUPF x) -> "HashUP \n" <>
-                       "  (" <> indentSansFirstLine 3 x <> ")"
-      (CheckUPF x y) -> "CheckUP" <> "\n" <>
-                        "  (" <> indentSansFirstLine 3 x <> ")\n" <>
-                        "  (" <> indentSansFirstLine 3 y <> ")"
+      (LeftUPF x) -> "LeftUP\n" <>
+                       "  " <> ind x
+      (RightUPF x) -> "RightUP\n" <>
+                        "  " <> ind x
+      (TraceUPF x) -> "TraceUP\n" <>
+                        "  " <> ind x
+      (UnsizedRecursionUPF x y z) -> "UnsizedRecursionUP\n" <>
+                        "  " <> ind x <> "\n" <>
+                        "  " <> ind y <> "\n" <>
+                        "  " <> ind z
+      (HashUPF x) -> "HashUP\n" <>
+                       "  " <> ind x
+      (CheckUPF x y) -> "CheckUP\n" <>
+                        "  " <> ind x <> "\n" <>
+                        "  " <> ind y
       (ListUPF []) -> "ListUP []"
       (ListUPF [x]) -> "ListUP [" <> x <> "]"
       (ListUPF ls) -> "ListUP\n" <>
-                        "  [" <> drop 3 (unlines (("  " <>) . indentSansFirstLine 4 . (", " <>) <$> ls)) <>
+                        concatMap (\x -> "  , " <> ind x <> "\n") ls <>
                         "  ]"
       (LetUPF ls x) -> "LetUP\n" <>
-                         "  [ " <> drop 4 (unlines ( ("  " <>)
-                                                   . indentSansFirstLine 3
-                                                   . (", " <>)
-                                                   . (\(x,y) -> "(" <> x <> ", " <> indentSansFirstLine (length x + 4) y <> ")")
-                                                   <$> ls
-                                                   )) <>
+                         concatMap (\(n,v) -> "  , (" <> n <> ", " <> ind v <> ")\n") ls <>
                          "  ]\n" <>
-                         "  (" <> indentSansFirstLine 3 x <> ")"
+                         "  " <> ind x
       (CaseUPF x ls) -> "CaseUP\n" <>
-                          "  (" <> indentSansFirstLine 3 x <> ")\n" <>
-                          "  [" <> drop 3 (unlines ( ("  " <>)
-                                                   . indentSansFirstLine 3
-                                                   . (", " <>)
-                                                   . (\(x,y) -> "(" <> show x <> ", " <> indentSansFirstLine ((length . show $ x) + 4) y <> ")")
-                                                   <$> ls
-                                                   )) <>
-                          "  ]\n"
+                          "  " <> ind x <> "\n" <>
+                          concatMap (\(p,v) -> "  , (" <> show p <> ",\n    " <> ind v <> ")\n") ls <>
+                          "  ]"
+      (UDTUPF ss x) -> "UDTUP " <> show ss <> "\n" <>
+                        "  " <> ind x
+      (ImportUPF s) -> "ImportUP " <> show s
+      (ImportQualifiedUPF s1 s2) -> "ImportQualifiedUP " <> show s1 <> " " <> show s2
 
 newtype PrettyUPT = PrettyUPT UnprocessedParsedTerm
 
diff --git a/src/Telomare.hs b/src/Telomare.hs
index 17200305..46e8972d 100644
--- a/src/Telomare.hs
+++ b/src/Telomare.hs
@@ -1046,12 +1046,12 @@ convertAbortMessage = \case
 -- |AST for patterns in `case` expressions
 data Pattern
   = PatternVar String
+  | PatternAnnotated Pattern UnprocessedParsedTerm
   | PatternInt Int
   | PatternString String
   | PatternIgnore
   | PatternPair Pattern Pattern
   deriving (Show, Eq, Ord)
-makeBaseFunctor ''Pattern
 
 -- |Firstly parsed AST sans location annotations
 data UnprocessedParsedTerm
@@ -1071,6 +1071,7 @@ data UnprocessedParsedTerm
   | TraceUP UnprocessedParsedTerm
   | CheckUP UnprocessedParsedTerm UnprocessedParsedTerm
   | HashUP UnprocessedParsedTerm -- ^ On ad hoc user defined types, this term will be substitued to a unique Int.
+  | UDTUP [String] UnprocessedParsedTerm
   | CaseUP UnprocessedParsedTerm [(Pattern, UnprocessedParsedTerm)]
   -- TODO: check if adding this doesn't create partial functions
   | ImportQualifiedUP String String
@@ -1079,6 +1080,8 @@ data UnprocessedParsedTerm
 makeBaseFunctor ''UnprocessedParsedTerm -- Functorial version UnprocessedParsedTerm
 makePrisms ''UnprocessedParsedTerm
 
+makeBaseFunctor ''Pattern
+
 instance Eq a => Eq (UnprocessedParsedTermF a) where
   (==) = eq1
 
@@ -1123,7 +1126,6 @@ instance Eq1 UnprocessedParsedTermF where
     mod1 == mod2
   liftEq _ _ _ = False
 
-
 instance (Show a) => Show (UnprocessedParsedTermF a) where
   show (VarUPF s) = "VarUPF " <> show s
   show (ITEUPF c t e) = "ITEUPF " <> show c <> " " <> show t <> " " <> show e
@@ -1141,7 +1143,10 @@ instance (Show a) => Show (UnprocessedParsedTermF a) where
   show (TraceUPF x) = "TraceUPF " <> show x
   show (CheckUPF a b) = "CheckUPF " <> show a <> " " <> show b
   show (HashUPF x) = "HashUPF " <> show x
+  show (UDTUPF ss x) = "UDTUPF " <> show ss <> " " <> show x
   show (CaseUPF scrutinee patterns) = "CaseUPF " <> show scrutinee <> " " <> show patterns
+  show (ImportQualifiedUPF s1 s2) = "ImportQualifiedUPF " <> show s1 <> " " <> show s2
+  show (ImportUPF s) = "ImportUPF " <> show s
 
 instance Show1 UnprocessedParsedTermF where
   liftShowsPrec showsPrecFunc showList d term = case term of
@@ -1179,6 +1184,7 @@ instance Show1 UnprocessedParsedTermF where
     CheckUPF a b -> showString "CheckUPF " . showsPrecFunc 11 a . showChar ' '
                     . showsPrecFunc 11 b
     HashUPF x -> showString "HashUPF " . showsPrecFunc 11 x
+    UDTUPF ss x -> showString "UDTUPF " . shows ss . showChar ' ' . showsPrecFunc 11 x
     CaseUPF scrutinee patterns ->
       let showPattern (pat, x) = showChar '(' . shows pat . showString ", "
                                 . showsPrecFunc 11 x . showChar ')'
diff --git a/src/Telomare/Parser.hs b/src/Telomare/Parser.hs
index ac64ad21..ccf0aa8b 100644
--- a/src/Telomare/Parser.hs
+++ b/src/Telomare/Parser.hs
@@ -6,9 +6,10 @@ module Telomare.Parser where
 
 import Control.Comonad.Cofree (Cofree (..), unwrap)
 import Control.Lens.Plated (Plated (..))
-import Control.Monad (void)
+import Control.Monad (join, void)
 import Control.Monad.State (State)
 import Data.Bifunctor (Bifunctor (first, second), bimap)
+import Data.Char (isUpper)
 import Data.Functor (($>))
 import Data.Functor.Foldable (Base, cata, para)
 import Data.Functor.Foldable.TH (MakeBaseFunctor (makeBaseFunctor))
@@ -34,6 +35,10 @@ import Text.Show.Deriving (deriveShow1)
 
 type AnnotatedUPT = Cofree UnprocessedParsedTermF LocTag
 
+data AssignmentEntry
+  = SingleAssignment String AnnotatedUPT
+  | ListAssignment LocTag [String] AnnotatedUPT
+
 instance Plated UnprocessedParsedTerm where
   plate f = \case
     ITEUP i t e -> ITEUP <$> f i <*> f t <*> f e
@@ -195,6 +200,15 @@ parseHash = do
   upt <- parseSingleExpr
   pure $ x :< HashUPF upt
 
+parseListAssignment :: TelomareParser AssignmentEntry
+parseListAssignment = do
+  x <- getLineColumn
+  names :: [String] <- (brackets (commaSep (scn *> identifier <* scn)) <* scn)
+                       <?> "list assignment names"
+  (scn *> symbol "=") <?> "list assignment ="
+  expr <- (scn *> parseLongExpr <* scn) <?> "list assignment body"
+  pure $ ListAssignment x names expr
+
 parseCase :: TelomareParser AnnotatedUPT
 parseCase = do
   x <- getLineColumn
@@ -214,6 +228,7 @@ parseSingleCase = do
 parsePattern :: TelomareParser Pattern
 parsePattern = choice $ try <$> [ parsePatternIgnore
                                 , parsePatternVar
+                                , parsePatternAnnotated
                                 , parsePatternString
                                 , parsePatternInt
                                 , parsePatternPair
@@ -233,11 +248,29 @@ parsePatternString :: TelomareParser Pattern
 parsePatternString = PatternString <$> (char '"' >> manyTill L.charLiteral (char '"'))
 
 parsePatternVar :: TelomareParser Pattern
-parsePatternVar = PatternVar <$> identifier
+parsePatternVar = PatternVar <$> (identifier <* scn)
+-- Pattern annotations are only accepted in parenthesised form
+-- (parsePatternAnnotated). Allowing a bare @v : T@ here would shadow
+-- the parenthesised path because parsePatternVar runs first in
+-- parsePattern's @choice@.
+
 
 parsePatternIgnore :: TelomareParser Pattern
 parsePatternIgnore = symbol "_" >> pure PatternIgnore
 
+-- |Parse a parenthesised pattern with a type/refinement annotation,
+-- e.g. @(aa : Nat)@. The stored typeExpr is the raw check function;
+-- 'buildMultiLambda' applies it to the bound value and uses the result as
+-- the case scrutinee, forcing runtime validation before destructuring.
+parsePatternAnnotated :: TelomareParser Pattern
+parsePatternAnnotated = parens body <?> "annotated pattern"
+  where
+    body = do
+      p <- (scn *> parsePattern <* scn) <?> "pattern before ':'"
+      symbol ":" <* scn
+      typeExpr <- (parseLongExpr <* scn) <?> "type expression after ':'"
+      pure $ PatternAnnotated p (forget typeExpr)
+
 -- |Parse a single expression.
 parseSingleExpr :: TelomareParser AnnotatedUPT
 parseSingleExpr = choice $ try <$> [ parseHash
@@ -262,16 +295,81 @@ parseApplied = do
       pure $ foldl (\a b -> x :< AppUPF a b) f args
     _ -> fail "expected expression"
 
+-- |Generate a fresh-looking variable name from a pattern's shape, used
+-- as the name of the lambda parameter that 'buildMultiLambda' introduces
+-- before destructuring.
+genPatternVarName :: Pattern -> String
+genPatternVarName = ("generatedVar" <>)
+                  . filter (\x -> x /= '\"'
+                               && x /= ' '
+                               && x /= '('
+                               && x /= ')'
+                               && x /= '['
+                               && x /= ']')
+                  . show
+
+-- |Pick the lambda-bound variable name for a pattern: use the user's name
+-- for a 'PatternVar', otherwise generate one.
+lambdaVarName :: Pattern -> String
+lambdaVarName = \case
+  PatternVar str -> str
+  p              -> genPatternVarName p
+
+-- |Build a multi-argument lambda whose destructuring all happens INSIDE
+-- the innermost lambda body. For @\\p1 p2 p3 -> body@ this emits
+--
+-- > \\v1 -> \\v2 -> \\v3 -> applyDestructure p3 v3
+-- >                                 (applyDestructure p2 v2
+-- >                                   (applyDestructure p1 v1 body))
+--
+-- where @applyDestructure p v body@ is @body@ when @p@ is a 'PatternVar'
+-- (no destructure needed) and a @case v of p -> body@ otherwise.
+--
+-- This avoids putting a function-valued lambda inside a case body, which
+-- would cause the case-rewrite to type-mismatch against the (Pair-typed)
+-- abort fallback.
+buildMultiLambda :: LocTag -> [Pattern] -> AnnotatedUPT -> AnnotatedUPT
+buildMultiLambda lt patterns body =
+  let varNames = lambdaVarName <$> patterns
+      destructured = foldr applyDestructure body (zip patterns varNames)
+      lamWrapped = foldr (\v inner -> lt :< LamUPF v inner) destructured varNames
+  in lamWrapped
+  where
+    applyDestructure :: (Pattern, String) -> AnnotatedUPT -> AnnotatedUPT
+    applyDestructure (p, varName) inner =
+      let bound = lt :< VarUPF varName
+          abort = lt :< AppUPF
+                    (lt :< VarUPF "abort")
+                    (lt :< StringUPF "buildMultiLambda: pattern not reached")
+      in case p of
+           PatternVar _ -> inner
+           PatternAnnotated innerPat typeExpr ->
+             -- Use the validator result as the case scrutinee instead of
+             -- CheckUPF: hash-based UDT validators are runtime values that
+             -- the static refinement analyzer cannot symbolically evaluate.
+             let tyApplied = lt :< AppUPF (tag lt typeExpr) bound
+             in lt :< CaseUPF tyApplied [(innerPat, inner)]
+           _ ->
+             lt :< CaseUPF bound
+               [ (p, inner)
+               , (PatternIgnore, abort)
+               ]
+
+-- |Build a single-argument lambda with optional destructuring.
+-- Kept as a thin wrapper around 'buildMultiLambda' so existing callers
+-- that work pattern-at-a-time continue to function.
+makeLambda :: LocTag -> Pattern -> AnnotatedUPT -> AnnotatedUPT
+makeLambda lt p = buildMultiLambda lt [p]
+
 -- |Parse lambda expression.
 parseLambda :: TelomareParser AnnotatedUPT
 parseLambda = do
   x <- getLineColumn
   symbol "\\" <* scn
-  variables <- some identifier <* scn
+  variables <- some parsePattern <* scn
   symbol "->" <* scn
-  -- TODO make sure lambda names don't collide with bound names
   term1expr <- parseLongExpr <* scn
-  pure $ foldr (\str upt -> x :< LamUPF str upt) term1expr variables
+  pure $ buildMultiLambda x variables term1expr
 
 -- |Parser that fails if indent level is not `pos`.
 parseSameLvl :: Pos -> TelomareParser a -> TelomareParser a
@@ -279,14 +377,17 @@ parseSameLvl pos parser = do
   lvl <- L.indentLevel
   if pos == lvl then parser else fail "Expected same indentation."
 
--- |Parse let expression.
+-- |Parse let expression. Accepts both plain @name = value@ assignments
+-- and list assignments @[n1, n2, ...] = value@. UDT declarations are
+-- a specialized list-assignment convention.
 parseLet :: TelomareParser AnnotatedUPT
 parseLet = do
   x <- getLineColumn
   reserved "let" <* scn
   lvl <- L.indentLevel
-  bindingsList <- manyTill (parseSameLvl lvl parseAssignment) (reserved "in") <* scn
+  entries <- manyTill (parseSameLvl lvl parseAssignmentEntry) (reserved "in") <* scn
   expr <- parseLongExpr <* scn
+  let bindingsList = entries >>= expandAssignmentEntry
   pure $ x :< LetUPF bindingsList expr
 
 -- |Parse long expression.
@@ -343,19 +444,172 @@ parseImportQualified = do
   qualifier <- identifier <* scn
   pure $ x :< ImportQualifiedUPF qualifier m
 
--- |Parse top level expressions.
+-- |A single top-level entry is either a name=value assignment or a list
+-- assignment `[n1, n2, …] = expr`. UDTs are recognized as a specialized
+-- uppercase-lambda list assignment during expansion.
+parseAssignmentEntry :: TelomareParser AssignmentEntry
+parseAssignmentEntry =
+  (uncurry SingleAssignment <$> parseAssignment)
+    <|> parseListAssignment
+
+-- |Parse assignments, expanding list assignments into their per-slot bindings.
+parseAssignmentEntries :: TelomareParser [(String, AnnotatedUPT)]
+parseAssignmentEntries = do
+  entries <- scn *> many parseAssignmentEntry <* eof
+  pure (expandAssignmentEntry =<< entries)
+
+-- |Parse top level expressions. Fails with a megaparsec error if the
+-- module has no @main@ definition, instead of crashing with 'fromJust'.
 parseTopLevelWithExtraModuleBindings :: [(String, AnnotatedUPT)]
                                      -> TelomareParser AnnotatedUPT
 parseTopLevelWithExtraModuleBindings lst = do
   x <- getLineColumn
-  bindingList <- scn *> many parseAssignment <* eof
-  pure $ x :< LetUPF (lst <> bindingList) (fromJust $ lookup "main" bindingList)
-
-parseDefinitions :: TelomareParser (AnnotatedUPT -> AnnotatedUPT)
-parseDefinitions = do
-  x <- getLineColumn
-  bindingList <- scn *> many parseAssignment <* eof
-  pure $ \y -> x :< LetUPF bindingList y
+  bindingList <- parseAssignmentEntries
+  case lookup "main" bindingList of
+    Just m  -> pure $ x :< LetUPF (lst <> bindingList) m
+    Nothing -> fail "missing 'main' definition"
+
+expandAssignmentEntry :: AssignmentEntry -> [(String, AnnotatedUPT)]
+expandAssignmentEntry = \case
+  SingleAssignment name body -> [(name, body)]
+  ListAssignment loc names body
+    | isUDTAssignment names body -> expandUDT (loc :< UDTUPF names body)
+    | otherwise                 -> expandPlainListAssignment loc names body
+
+isUDTAssignment :: [String] -> AnnotatedUPT -> Bool
+isUDTAssignment (name:_) (_ :< LamUPF _ _) = case name of
+  firstChar:_ -> isUpper firstChar
+  _           -> False
+isUDTAssignment _ _ = False
+
+expandPlainListAssignment :: LocTag -> [String] -> AnnotatedUPT -> [(String, AnnotatedUPT)]
+expandPlainListAssignment loc names body =
+  case listAssignmentSlots body of
+    Just (slots, wrapBody)
+      | length names == length slots -> zip names (wrapBody <$> slots)
+      | otherwise -> error
+        $ "list assignment arity mismatch: " <> show (length names)
+        <> " names for " <> show (length slots) <> " values"
+    Nothing ->
+      let intermediate = listAssignmentIntermediate loc
+          source = loc :< VarUPF intermediate
+          mkAccessorBinding idx name = (name, accessAt loc idx source)
+      in (intermediate, body) : zipWith mkAccessorBinding [0 ..] names
+
+-- |Find a final list literal in a plain list assignment, preserving lambdas
+-- and lets around each extracted slot. This lets `[f, g] = \x -> [...]`
+-- bind `f` and `g` as functions rather than trying to project from a lambda.
+listAssignmentSlots :: AnnotatedUPT -> Maybe ([AnnotatedUPT], AnnotatedUPT -> AnnotatedUPT)
+listAssignmentSlots = go where
+  go (l :< ListUPF xs) = Just (xs, id)
+  go (l :< LetUPF binds inner) = do
+    (xs, wrapBody) <- go inner
+    pure (xs, \expr -> l :< LetUPF binds (wrapBody expr))
+  go (l :< LamUPF var inner) = do
+    (xs, wrapBody) <- go inner
+    pure (xs, \expr -> l :< LamUPF var (wrapBody expr))
+  go _ = Nothing
+
+listAssignmentIntermediate :: LocTag -> String
+listAssignmentIntermediate = \case
+  Loc line column -> "__list_assignment_" <> show line <> "_" <> show column
+  DummyLoc        -> "__list_assignment"
+
+accessAt :: LocTag -> Int -> AnnotatedUPT -> AnnotatedUPT
+accessAt loc 0 e = loc :< LeftUPF e
+accessAt loc n e = loc :< LeftUPF (iterate (\x -> loc :< RightUPF x) e !! n)
+
+-- |Expand a UDT declaration into a list of top-level bindings.
+--
+-- If the UDT body is a lambda @\\h -> ...@ (the canonical UDT idiom),
+-- the expansion automatically wraps the core type representation with
+-- the hash-tag mechanism (@wrapper (# wrapper)@). The shared core tuple
+-- contains only the generated hash, the auto-generated validator, and
+-- the first two user slots (constructor/extractor by convention).
+-- Remaining slots are hoisted to normal top-level bindings so using a
+-- constructor or extractor does not force every operation through sizing.
+--
+-- > [T, mk, unT, op1, ...] = \\h -> [ mkBody, unTBody, op1Body, ... ]
+--
+-- becomes (conceptually):
+--
+-- > __udt_T = wrapper (# wrapper)
+-- >   where wrapper = \\h -> let T = validatorFor T h in [h, T, mkBody, unTBody]
+-- > __udt_T_hash = left __udt_T
+-- > T   = left (right __udt_T)   -- validator, usable as `(x : T)` outside
+-- > mk  = left (right (right __udt_T))
+-- > unT = left (right (right (right __udt_T)))
+-- > op1 = let h = __udt_T_hash; T = validatorFor T h in op1Body
+--
+-- Non-lambda list assignments use 'expandPlainListAssignment' instead;
+-- this fallback is kept for direct/internal callers of 'expandUDT'.
+expandUDT :: AnnotatedUPT -> [(String, AnnotatedUPT)]
+expandUDT (loc :< UDTUPF names@(tname:_) body) =
+  case body of
+    (_ :< LamUPF hParam inner) ->
+      let (slots, wrapBody) = udtSlots tname inner
+          (coreSlots, hoistedSlots) = splitAt 2 slots
+          coreNames = take (1 + length coreSlots) names
+          hoistedNames = drop (1 + length coreSlots) names
+          validator    = autoValidator loc tname hParam
+          intermediate = "__udt_" <> tname
+          hashName     = intermediate <> "_hash"
+          hashVar      = loc :< VarUPF hashName
+          coreList     = loc :< ListUPF ((loc :< VarUPF hParam)
+                                      : (loc :< VarUPF tname)
+                                      : coreSlots)
+          wrappedInner = loc :< LetUPF [(tname, validator)] (wrapBody coreList)
+          wrapper      = loc :< LamUPF hParam wrappedInner
+          udtTuple     = loc :< AppUPF wrapper (loc :< HashUPF wrapper)
+          hashBinding  = (hashName, accessAt loc 0 (loc :< VarUPF intermediate))
+          mkAccessorBinding idx name =
+            (name, accessAt loc idx (loc :< VarUPF intermediate))
+          mkHoistedBinding name slot =
+            ( name
+            , loc :< LetUPF [ (hParam, hashVar)
+                            , (tname, validator)
+                            ]
+                (wrapBody slot)
+            )
+      in (intermediate, udtTuple)
+       : hashBinding
+       : zipWith mkAccessorBinding [1 ..] coreNames
+      <> zipWith mkHoistedBinding hoistedNames hoistedSlots
+    _ ->
+      zipWith (\name idx -> (name, accessAt loc idx body)) names [0 ..]
+expandUDT _ = []
+
+-- |Find the final list literal in a UDT body and return a wrapper that
+-- reapplies any surrounding lets. Hoisted methods get the same let
+-- context as the core tuple, but not the sibling method bodies.
+udtSlots :: String -> AnnotatedUPT -> ([AnnotatedUPT], AnnotatedUPT -> AnnotatedUPT)
+udtSlots tname = go where
+  go (l :< ListUPF xs) = (xs, id)
+  go (l :< LetUPF binds inner) =
+    let (xs, wrapBody) = go inner
+    in (xs, \expr -> l :< LetUPF binds (wrapBody expr))
+  go (_ :< other) = error
+    $ "expandUDT: UDT body for [" <> tname
+    <> "] must reduce to a list literal; got: " <> show (void other)
+
+-- |Auto-generated validator: @\\v -> if dEqual (left v) <h> then right v else abort \"not <T>\"@.
+-- Returns the validated payload on success; aborts on failure.
+-- Annotated pattern lambdas use the validator's result as the case
+-- scrutinee, so destructuring works on a validated value without an
+-- extra ITE.
+autoValidator :: LocTag -> String -> String -> AnnotatedUPT
+autoValidator loc tname hParam =
+  loc :< LamUPF "__udt_v"
+    (loc :< ITEUPF
+       (loc :< AppUPF
+          (loc :< AppUPF
+             (loc :< VarUPF "dEqual")
+             (loc :< LeftUPF (loc :< VarUPF "__udt_v")))
+          (loc :< VarUPF hParam))
+       (loc :< RightUPF (loc :< VarUPF "__udt_v"))
+        (loc :< AppUPF
+           (loc :< VarUPF "abort")
+           (loc :< StringUPF ("not " <> tname))))
 
 -- |Helper function to test parsers without a result.
 runTelomareParser_ :: Show a => TelomareParser a -> String -> IO ()
@@ -386,20 +640,21 @@ runParseLongExpr str = bimap errorBundlePretty forget' $ runParser parseLongExpr
     forget' = forget
 
 parsePrelude :: String -> Either String [(String, AnnotatedUPT)]
-parsePrelude str = let result = runParser (scn *> many parseAssignment <* eof) "" str
+parsePrelude str = let result = runParser parseAssignmentEntries "" str
                     in first errorBundlePretty result
 
-parseImportOrAssignment :: TelomareParser (Either AnnotatedUPT (String, AnnotatedUPT))
+-- |One parser step inside a module: returns a list because list assignments
+-- expand into multiple (name, value) bindings.
+parseImportOrAssignment :: TelomareParser [Either AnnotatedUPT (String, AnnotatedUPT)]
 parseImportOrAssignment = do
-  x <- getLineColumn
   maybeImport <- optional $ scn *> (try parseImportQualified <|> try parseImport) <* scn
   case maybeImport of
     Nothing -> do
-      maybeAssignment <- optional $ scn *> try parseAssignment <* scn
-      case maybeAssignment of
-        Nothing -> fail "Expected either an import statement or an assignment"
-        Just a  -> pure $ Right a
-    Just imp -> pure $ Left imp
+      maybeEntry <- optional $ scn *> try parseAssignmentEntry <* scn
+      case maybeEntry of
+        Nothing    -> fail "Expected either an import statement or an assignment"
+        Just entry -> pure (Right <$> expandAssignmentEntry entry)
+    Just imp -> pure [Left imp]
 
 parseWithPrelude :: [(String, AnnotatedUPT)]   -- ^Prelude
                  -> String                     -- ^Raw string to be parsed
@@ -407,7 +662,7 @@ parseWithPrelude :: [(String, AnnotatedUPT)]   -- ^Prelude
 parseWithPrelude prelude str = first errorBundlePretty $ runParser (parseTopLevelWithExtraModuleBindings prelude) "" str
 
 parseModule :: String -> Either String [Either AnnotatedUPT (String, AnnotatedUPT)]
-parseModule str = let result = runParser (scn *> many parseImportOrAssignment <* eof) "" str
+parseModule str = let result = runParser (concat <$> (scn *> many parseImportOrAssignment <* eof)) "" str
                   in first errorBundlePretty result
 
 -- |Parse either a single expression or top level definitions defaulting to the `main` definition.
diff --git a/src/Telomare/Resolver.hs b/src/Telomare/Resolver.hs
index f425412c..6b70d650 100644
--- a/src/Telomare/Resolver.hs
+++ b/src/Telomare/Resolver.hs
@@ -73,9 +73,10 @@ findInts anno = cata alg where
   alg :: Base Pattern [AnnotatedUPT -> AnnotatedUPT]
       -> [AnnotatedUPT -> AnnotatedUPT]
   alg = \case
-    PatternPairF x y -> ((. (anno :< ) . LeftUPF) <$> x) <> ((. (anno :< ) . RightUPF) <$> y)
-    PatternIntF x    -> [id]
-    _                -> []
+    PatternPairF x y      -> ((. (anno :< ) . LeftUPF) <$> x) <> ((. (anno :< ) . RightUPF) <$> y)
+    PatternIntF x         -> [id]
+    PatternAnnotatedF x _ -> x
+    _                     -> []
 
 -- | Finds all PatternString leaves returning "directions" to these leaves through pairs
 -- in the form of a combination of RightUP and LeftUP from the root
@@ -86,9 +87,10 @@ findStrings anno = cata alg where
   alg :: Base Pattern [AnnotatedUPT -> AnnotatedUPT]
       -> [AnnotatedUPT -> AnnotatedUPT]
   alg = \case
-    PatternPairF x y -> ((. (anno :< ) . LeftUPF) <$> x) <> ((. (anno :< ) . RightUPF) <$> y)
-    PatternStringF x -> [id]
-    _                -> []
+    PatternPairF x y      -> ((. (anno :< ) . LeftUPF) <$> x) <> ((. (anno :< ) . RightUPF) <$> y)
+    PatternStringF x      -> [id]
+    PatternAnnotatedF x _ -> x
+    _                     -> []
 
 fitPatternVarsToCasedUPT :: Pattern -> AnnotatedUPT -> AnnotatedUPT
 fitPatternVarsToCasedUPT p aupt@(anno :< _) = applyVars2UPT varsOnUPT $ pattern2UPT anno p where
@@ -114,6 +116,40 @@ varsUPT = cata alg where
   del :: String -> Set String -> Set String
   del n x = if Set.member n x then Set.delete n x else x
 
+-- |Like 'varsUPT' but also descends into 'Pattern' type annotations so that
+-- names referenced via @: T@ patterns (e.g. UDT validators) are included.
+freeVarsDeep :: UnprocessedParsedTerm -> Set String
+freeVarsDeep = cata alg where
+  alg :: Base UnprocessedParsedTerm (Set String) -> Set String
+  alg (VarUPF n)           = Set.singleton n
+  alg (LamUPF n body)      = Set.delete n body
+  alg (CaseUPF scrut alts) = scrut <> foldMap (\(p, body) -> patternRefs p <> body) alts <> caseRefs
+    where
+      caseRefs = Set.fromList ["and", "listEqual", "foldl", "abort"]
+  alg e                    = F.fold e
+
+  patternRefs :: Pattern -> Set String
+  patternRefs = cata palg where
+    palg :: Base Pattern (Set String) -> Set String
+    palg (PatternAnnotatedF inner ty) = inner <> freeVarsDeep ty
+    palg e                            = F.fold e
+
+-- |Keep only bindings transitively reachable from @root@. Unreachable
+-- bindings are skipped by 'process' and 'compile', giving large speedups
+-- when a snippet only uses a small slice of a large Prelude+UDT environment.
+--
+-- 'freeVarsDeep' also accounts for names that 'removeCaseUPs' (called
+-- inside 'process') injects into case alternatives: @and@, @listEqual@,
+-- @foldl@, @abort@. Without these the pruned LetUPF would fail with
+-- MissingDefinitions after case expansion.
+pruneBindings :: AnnotatedUPT -> [(String, AnnotatedUPT)] -> [(String, AnnotatedUPT)]
+pruneBindings root bs = filter ((`Set.member` reachable) . fst) bs
+  where
+    seed      = freeVarsDeep (forget root)
+    bmap      = Map.fromList $ fmap (second (freeVarsDeep . forget)) bs
+    expand r  = r <> F.fold (Map.restrictKeys bmap r)
+    reachable = until (\s -> expand s == s) expand seed
+
 mkLambda4FreeVarUPs :: AnnotatedUPT -> AnnotatedUPT
 mkLambda4FreeVarUPs aupt@(anno :< _) = tag anno $ go upt freeVars where
   upt = forget aupt
@@ -128,9 +164,10 @@ findPatternVars anno = cata alg where
   alg :: Base Pattern (Map String (AnnotatedUPT -> AnnotatedUPT))
       -> Map String (AnnotatedUPT -> AnnotatedUPT)
   alg = \case
-    PatternPairF x y -> ((. (anno :< ). LeftUPF) <$> x) <> ((. (anno :< ). RightUPF) <$> y)
-    PatternVarF str  -> Map.singleton str id
-    _                -> Map.empty
+    PatternPairF x y      -> ((. (anno :< ). LeftUPF) <$> x) <> ((. (anno :< ). RightUPF) <$> y)
+    PatternVarF str       -> Map.singleton str id
+    PatternAnnotatedF x _ -> x
+    _                     -> Map.empty
 
 -- TODO: Annotate without so much fuzz
 pairStructureCheck :: Pattern -> UnprocessedParsedTerm -> UnprocessedParsedTerm
@@ -145,18 +182,20 @@ pairRoute2Dirs = cata alg where
   alg :: Base Pattern [UnprocessedParsedTerm -> UnprocessedParsedTerm]
       -> [UnprocessedParsedTerm -> UnprocessedParsedTerm]
   alg = \case
-    PatternPairF x y -> [id] <> ((. LeftUP) <$> x) <> ((. RightUP) <$> y)
-    _                -> []
+    PatternPairF x y      -> [id] <> ((. LeftUP) <$> x) <> ((. RightUP) <$> y)
+    PatternAnnotatedF x _ -> x
+    _                     -> []
 
 pattern2UPT :: LocTag -> Pattern -> AnnotatedUPT
 pattern2UPT anno = tag anno . cata alg where
   alg :: Base Pattern UnprocessedParsedTerm -> UnprocessedParsedTerm
   alg = \case
-    PatternPairF x y   -> PairUP x y
-    PatternIntF i      -> IntUP i
-    PatternStringF str -> StringUP str
-    PatternVarF str    -> IntUP 0
-    PatternIgnoreF     -> IntUP 0
+    PatternPairF x y       -> PairUP x y
+    PatternIntF i          -> IntUP i
+    PatternStringF str     -> StringUP str
+    PatternVarF str        -> IntUP 0
+    PatternIgnoreF         -> IntUP 0
+    PatternAnnotatedF x _  -> x
       -- Note that "__ignore" is a special variable name and not accessible to users because
       -- parsing of VarUPs doesn't allow variable names to start with `_`
 
@@ -369,15 +408,21 @@ validateVariables term =
                 [(name, Set.fromList $ getDirectDeps def) | (name, def) <- preludeMap]
 
               -- Get direct variable dependencies (only those defined in this let block)
+              -- Uses Set to properly handle lambda-bound variable shadowing
+              letBindingNames = Set.fromList (fmap fst preludeMap)
               getDirectDeps :: AnnotatedUPT -> [String]
-              getDirectDeps = cata alg where
-                alg :: CofreeF UnprocessedParsedTermF LocTag [String] -> [String]
+              getDirectDeps = Set.toList . cata alg where
+                alg :: CofreeF UnprocessedParsedTermF LocTag (Set String) -> Set String
                 alg = \case
-                    (_ C.:< VarUPF n) -> [n | any ((== n) . fst) preludeMap]
-                    (_ C.:< LamUPF _ body) -> body
+                    (_ C.:< VarUPF n) -> if Set.member n letBindingNames then Set.singleton n else Set.empty
+                    (_ C.:< LamUPF v body) -> Set.delete v body
+                    (_ C.:< LetUPF binds body) ->
+                      let boundNames = Set.fromList (fmap fst binds)
+                          bindDeps = foldMap snd binds
+                      in Set.union (bindDeps Set.\\ boundNames) (body Set.\\ boundNames)
                     (_ C.:< ITEUPF i t e) -> i <> t <> e
                     (_ C.:< PairUPF a b) -> a <> b
-                    (_ C.:< ListUPF l) -> concat l
+                    (_ C.:< ListUPF l) -> F.fold l
                     (_ C.:< AppUPF f x) -> f <> x
                     (_ C.:< UnsizedRecursionUPF t r b) -> t <> r <> b
                     (_ C.:< LeftUPF x) -> x
@@ -385,7 +430,7 @@ validateVariables term =
                     (_ C.:< TraceUPF x) -> x
                     (_ C.:< CheckUPF cf x) -> cf <> x
                     (_ C.:< HashUPF x) -> x
-                    _ -> []
+                    _ -> Set.empty
 
           -- Check if original order works (no forward references)
           let originalOrder = fmap fst preludeMap
@@ -734,7 +779,7 @@ resolveMain allModules mainModule = case lookup mainModule allModules of
                   maybeMain = lookup "main" resolved
               in case maybeMain of
                    Nothing -> Left $ NoMainFunction mainModule
-                   Just x  -> Right $ DummyLoc :< LetUPF resolved x
+                   Just x  -> Right $ DummyLoc :< LetUPF (pruneBindings x resolved) x
 
 main2Term3 :: [(String, [Either AnnotatedUPT (String, AnnotatedUPT)])] -- ^Modules: [(ModuleName, [Either Import (VariableName, BindedUPT)])]
            -> String -- ^Module name with main
diff --git a/telomare.cabal b/telomare.cabal
index 8bd9ccdd..17436fc0 100644
--- a/telomare.cabal
+++ b/telomare.cabal
@@ -281,11 +281,12 @@ test-suite telomare-sizing-test
   ghc-options:         -threaded -rtsopts -with-rtsopts=-N
   default-language:    Haskell2010
 
-test-suite telomare-arithmetic-test
+test-suite telomare-udt-test
   type:                exitcode-stdio-1.0
   hs-source-dirs:      test
-  main-is:             ArithmeticTests.hs
+  main-is:             UDTTests.hs
   other-modules:       Common
+                     , NatUDTTests
   build-depends:       base
                      , containers
                      , free
diff --git a/test/NatUDTTests.hs b/test/NatUDTTests.hs
new file mode 100644
index 00000000..ceb47dc3
--- /dev/null
+++ b/test/NatUDTTests.hs
@@ -0,0 +1,166 @@
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PartialTypeSignatures #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+
+-- | Dedicated tests for the user-defined-type sugar
+-- @[T, op1, op2, ...] = \\h -> [ ... ]@ exercised through an embedded
+-- @Nat@ UDT fixture.
+module NatUDTTests (natUDTTests) where
+
+import Control.Comonad.Cofree (Cofree ((:<)))
+import Control.Monad (unless)
+import Data.Bifunctor (Bifunctor (first))
+import Data.List (isInfixOf)
+import PrettyPrint
+import qualified System.IO.Strict as Strict
+import Telomare
+import Telomare.Eval (SizingOption (..), compile, runStaticChecks)
+import Telomare.Parser (AnnotatedUPT, parseLongExpr, parsePrelude)
+import Telomare.Possible (SizingSettings (SizingSettings))
+import Telomare.PossibleData (CompiledExpr)
+import Telomare.Resolver (process, pruneBindings)
+import Test.Tasty
+import Test.Tasty.HUnit
+import Text.Megaparsec (eof, errorBundlePretty, runParser)
+
+natUDTSource :: String
+natUDTSource = unlines
+  [ "[Nat, toNat, fromNat, nPlus, nMinus] = \\h ->"
+  , "  [ \\x -> (h, x)"
+  , "  , \\(x : Nat) -> x"
+  , "  , \\(aa : Nat) (bb : Nat) -> (h, d2c aa succ bb)"
+  , "  , \\(aa : Nat) (bb : Nat) ->"
+  , "      let sLeft = \\x -> case x of"
+  , "                          (l, _) -> l"
+  , "                          y      -> abort \"can't subtract larger number from smaller one\""
+  , "      in (h, d2c bb sLeft aa)"
+  , "  ]"
+  ]
+
+parseBindings :: String -> String -> IO [(String, AnnotatedUPT)]
+parseBindings name raw =
+  case parsePrelude raw of
+    Left err -> error $ "parseBindings: " <> name <> ": " <> err
+    Right bs -> pure bs
+
+loadBindings :: FilePath -> IO [(String, AnnotatedUPT)]
+loadBindings path = do
+  raw <- Strict.readFile path
+  parseBindings path raw
+
+-- |Evaluate @expr@ in the scope of @Prelude.tel@ + the embedded Nat UDT.
+evalUDTExpr :: String -> IO (Either String String)
+evalUDTExpr input = do
+  preludeBindings <- loadBindings "Prelude.tel"
+  udtBindings     <- parseBindings "Nat UDT fixture" natUDTSource
+  let allBindings = preludeBindings <> udtBindings
+  case runParser (parseLongExpr <* eof) "" input of
+    Left err -> pure $ Left (errorBundlePretty err)
+    Right aupt -> do
+      let term = DummyLoc :< LetUPF (pruneBindings aupt allBindings) aupt
+          compile' :: Term3 -> Either EvalError CompiledExpr
+          compile' = compile (DebugSizing (SizingSettings 255 False)) runStaticChecks
+      case first RE (process term) >>= compile' of
+        Left err -> pure $ Left (show err)
+        Right iexpr -> case eval iexpr of
+          Left e       -> pure . Left . show $ e
+          Right result -> case toTelomare result of
+            Just r  -> pure . Right . show $ PrettyIExpr r
+            Nothing -> pure . Left $ "conversion error from result:\n" <> prettyPrint result
+
+assertEvalEquals :: String -> String -> Assertion
+assertEvalEquals input expected = do
+  res <- evalUDTExpr input
+  case res of
+    Left err  -> unless (expected `isInfixOf` err) . assertFailure
+                  $ "Evaluation failed: " <> err
+    Right val -> val @?= expected
+
+assertAborts :: String -> String -> Assertion
+assertAborts input msgFragment = do
+  res <- evalUDTExpr input
+  case res of
+    Left err ->
+      unless ("abort:" `isInfixOf` err && msgFragment `isInfixOf` err)
+        . assertFailure
+        $ "Expected abort containing '" <> msgFragment <> "', got: " <> err
+    Right val ->
+      assertFailure
+        $ "Expected abort containing '" <> msgFragment
+        <> "' but evaluation succeeded with: " <> val
+
+assertStaticCheckError :: String -> String -> Assertion
+assertStaticCheckError input msgFragment = do
+  res <- evalUDTExpr input
+  case res of
+    Left err ->
+      unless ("StaticCheckError" `isInfixOf` err && msgFragment `isInfixOf` err)
+        . assertFailure
+        $ "Expected static check error containing '" <> msgFragment <> "', got: " <> err
+    Right val ->
+      assertFailure
+        $ "Expected static check error containing '" <> msgFragment
+        <> "' but evaluation succeeded with: " <> val
+
+natUDTTests :: TestTree
+natUDTTests = testGroup "User-defined-type sugar (embedded Nat UDT)"
+  [ testGroup "Unit tests"
+      [ testCase "toNat then right round-trips the value" $
+          assertEvalEquals "right (toNat 8)" "8"
+      , testCase "fromNat extracts a Nat payload" $
+          assertEvalEquals "fromNat (toNat 8)" "8"
+      , testCase "nPlus on two valid Nats returns the sum" $
+          assertEvalEquals "right (nPlus (toNat 3) (toNat 5))" "8"
+      , testCase "nMinus on two valid Nats returns the difference" $
+          assertEvalEquals "right (nMinus (toNat 7) (toNat 2))" "5"
+      , testCase "nMinus aborts on underflow" $
+          assertAborts
+            "right (nMinus (toNat 2) (toNat 7))"
+            "can't subtract larger number from smaller one"
+      , testCase "nPlus rejects a non-Nat first arg" $
+          assertAborts
+            "right (nPlus (0, 3) (toNat 5))"
+            "not Nat"
+      , testCase "nPlus rejects a non-Nat second arg" $
+          assertAborts
+            "right (nPlus (toNat 3) (0, 5))"
+            "not Nat"
+      , testCase "UDT destructuring works inside let" $
+          assertEvalEquals
+            ( "let [Color, mkColor, defaultColor] = \\h -> "
+              <> "[ \\c -> (h, c), (h, 7) ] "
+              <> "in right defaultColor" )
+            "7"
+      , testCase "plain list assignment works inside let" $
+          assertEvalEquals
+            "let [a, b, c] = [1, 2, 3] in b"
+            "2"
+      -- Normal refinement annotations, such as @x : validator = value@,
+      -- still lower to @CheckUPF@. The compiler's static refinement pass
+      -- runs that validator symbolically and rejects values that can be
+      -- proven to abort.
+      --
+      -- UDT pattern annotations, such as @\(x : Nat) -> x@, deliberately do
+      -- not lower to @CheckUPF@. A UDT validator compares the branded value's
+      -- hash against the UDT hash generated by the UDT expansion, so the
+      -- static refinement analyzer cannot prove it symbolically. Instead the
+      -- parser lowers the annotation to a runtime validator call used as a
+      -- @case@ scrutinee: success extracts the payload, and failure aborts at
+      -- runtime with the validator's message.
+      , testCase "plain refinement annotations use static CheckUPF" $
+          assertStaticCheckError
+            ( "let x : (\\v -> assert (not v) "
+              <> "\"plain refinement uses CheckUPF\") = 1 in x" )
+            "plain refinement uses CheckUPF"
+      , testCase "UDT annotations validate branded values at runtime" $
+          assertEvalEquals "fromNat (toNat 8)" "8"
+      , testCase "UDT annotations reject unbranded values at runtime" $
+          assertAborts "fromNat (0, 8)" "not Nat"
+      ]
+  -- NOTE: QuickCheck property tests for nPlus/nMinus were omitted
+  -- because each evalUDTExpr call recompiles Prelude+the embedded UDT+the
+  -- expression from scratch, which currently takes 5–6 minutes per
+  -- compile (Prelude is big; nPlus pulls in the d2c recursion which
+  -- triggers sizing). The unit tests above cover the same behaviour.
+  ]
diff --git a/test/ResolverTests.hs b/test/ResolverTests.hs
index 66f1fdaf..68254040 100644
--- a/test/ResolverTests.hs
+++ b/test/ResolverTests.hs
@@ -336,6 +336,12 @@ unitTests = testGroup "Unit tests"
   , testCase "Ad hoc user defined types failure" $ do
       res <- testUserDefAdHocTypes userDefAdHocTypesFailure
       res @?= "MyInt must not be 0\ndone"
+  , testCase "plain top-level list assignment" $ do
+      res <- testUserDefAdHocTypes topLevelListAssignment
+      res @?= "right\ndone"
+  , testCase "lowercase lambda list assignment is not a UDT" $ do
+      res <- testUserDefAdHocTypes lambdaListAssignment
+      res @?= "kept\ndone"
   , testCase "test tictactoe.tel" $ do
       res <- tictactoe
       res @?= fullRunTicTacToeString
@@ -465,28 +471,36 @@ testUserDefAdHocTypes input = do
 
 userDefAdHocTypesSuccess = unlines
   [ "import Prelude"
-  , "MyInt = let wrapper = \\h -> ( \\i -> if not i"
-  , "                                      then \"MyInt must not be 0\""
-  , "                                      else  i"
-  , "                             , \\i -> if dEqual (left i) h"
-  , "                                      then 0"
-  , "                                      else \"expecting MyInt\""
-  , "                             )"
-  , "        in wrapper (# wrapper)"
-  , "main = \\i -> ((left MyInt) 8, 0)"
+  , "[MyInt, mkMyInt, unMyInt] = \\h ->"
+  , "  [ \\i -> if not i"
+  , "          then \"MyInt must not be 0\""
+  , "          else (h, i)"
+  , "  , \\(i : MyInt) -> i"
+  , "  ]"
+  , "main = \\i -> (unMyInt (mkMyInt 8), 0)"
   ]
 
 userDefAdHocTypesFailure = unlines
   [ "import Prelude"
-  , "MyInt = let wrapper = \\h -> ( \\i -> if not i"
-  , "                                      then \"MyInt must not be 0\""
-  , "                                      else  i"
-  , "                             , \\i -> if dEqual (left i) h"
-  , "                                      then 0"
-  , "                                      else \"expecting MyInt\""
-  , "                             )"
-  , "        in wrapper (# wrapper)"
-  , "main = \\i -> ((left MyInt) 0, 0)"
+  , "[MyInt, mkMyInt, unMyInt] = \\h ->"
+  , "  [ \\i -> if not i"
+  , "          then \"MyInt must not be 0\""
+  , "          else (h, i)"
+  , "  , \\(i : MyInt) -> i"
+  , "  ]"
+  , "main = \\i -> (mkMyInt 0, 0)"
+  ]
+
+topLevelListAssignment = unlines
+  [ "import Prelude"
+  , "[a, b] = [\"left\", \"right\"]"
+  , "main = \\i -> (b, 0)"
+  ]
+
+lambdaListAssignment = unlines
+  [ "import Prelude"
+  , "[f, g] = \\x -> [\\y -> x, \\z -> z]"
+  , "main = \\i -> (f \"kept\" 0, 0)"
   ]
 
 hashtest0 = unlines ["let wrapper = 2",
diff --git a/test/ArithmeticTests.hs b/test/UDTTests.hs
similarity index 94%
rename from test/ArithmeticTests.hs
rename to test/UDTTests.hs
index 0f668de6..f70ae875 100644
--- a/test/ArithmeticTests.hs
+++ b/test/UDTTests.hs
@@ -12,6 +12,7 @@ import Data.Bifunctor (Bifunctor (first))
 import Data.List (isInfixOf)
 import Data.Ratio
 import Debug.Trace
+import NatUDTTests (natUDTTests)
 import PrettyPrint
 import qualified System.IO.Strict as Strict
 import Telomare
@@ -21,7 +22,7 @@ import Telomare.Parser (AnnotatedUPT, TelomareParser, parseLongExpr,
                         parsePrelude)
 import Telomare.Possible (SizingSettings (SizingSettings))
 import Telomare.PossibleData (CompiledExpr)
-import Telomare.Resolver (process)
+import Telomare.Resolver (process, pruneBindings)
 import Telomare.RunTime (simpleEval)
 import Test.Tasty
 import Test.Tasty.HUnit
@@ -33,11 +34,12 @@ main :: IO ()
 main = defaultMain tests
 
 tests :: TestTree
-tests = testGroup "Arithmetic Tests" [ unitTestsNatArithmetic
-                                     , unitTestsRatArithmetic
-                                     , qcPropsNatArithmetic
-                                     , qcPropsRatArithmetic
-                                     ]
+tests = testGroup "UDT Tests" [ unitTestsNatArithmetic
+                              , unitTestsRatArithmetic
+                              , qcPropsNatArithmetic
+                              , qcPropsRatArithmetic
+                              , natUDTTests
+                              ]
 
 maybeToRight :: Maybe a -> Either EvalError a
 maybeToRight (Just x) = Right x
@@ -61,7 +63,7 @@ evalExprString input = do
   case parseResult of
     Left err -> pure $ Left (errorBundlePretty err)
     Right aupt -> do
-      let term = DummyLoc :< LetUPF preludeBindings aupt
+      let term = DummyLoc :< LetUPF (pruneBindings aupt preludeBindings) aupt
           compile' :: Term3 -> Either EvalError CompiledExpr
           compile' = compile (DebugSizing (SizingSettings 255 False)) runStaticChecks
       case first RE (process term) >>= compile' of