diff --git a/TODO.md b/TODO.md
index c2e9d27..2f6fcd5 100644
--- a/TODO.md
+++ b/TODO.md
@@ -228,10 +228,6 @@
   - This may need a little care. But I think I could collect all constructors that only match wildcards into a single case. This would lose any information from breaking out the individual, unnamed cases though.
   - There are cases where we have  `_` and then `Foo` on the next line, but they should all get collected into the `Foo` case. I think I sorted all of this out for primitives.
 - [x] Case for primitives
-- [ ] aoc2023 translation
-  - [x] day1
-  - [x] day2 - day6
-  - some "real world" examples
 - [x] Maybe Eq and stuff would work for typeclass without dealing with unification issues yet
 - [x] unsolved meta errors repeat (need to freeze or only report at end)
 - [x] Sanitize JS idents, e.g. `_+_`
diff --git a/aoc2023/Day1.newt b/aoc2023/Day1.newt
deleted file mode 100644
index 6e368ec..0000000
--- a/aoc2023/Day1.newt
+++ /dev/null
@@ -1,62 +0,0 @@
-module Day1
-
-import Prelude
-import Node
-
-digits1 : List Char -> List Int
-digits1 Nil = Nil
-digits1 (c :: cs) = let x = ord c in
-  if 48 < x && x < 58
-    then x - 48 :: digits1 cs
-    else digits1 cs
-
--- TODO I used @ patterns in Lean
-digits2 : List Char -> List Int
-digits2 xs = case xs of
-    ('o' :: 'n' :: 'e' :: _) => 1 :: digits2 (tail xs)
-    ('t' :: 'w' :: 'o' :: _) => 2 :: digits2 (tail xs)
-    ('t' :: 'h' :: 'r' :: 'e' :: 'e' :: _) => 3 :: digits2 (tail xs)
-    ('f' :: 'o' :: 'u' :: 'r' :: _) => 4 :: digits2 (tail xs)
-    ('f' :: 'i' :: 'v' :: 'e' :: _) => 5 :: digits2 (tail xs)
-    ('s' :: 'i' :: 'x' :: _) => 6 :: digits2 (tail xs)
-    ('s' :: 'e' :: 'v' :: 'e' :: 'n' :: _) => 7 :: digits2 (tail xs)
-    ('e' :: 'i' :: 'g' :: 'h' :: 't' :: _) => 8 :: digits2 (tail xs)
-    ('n' :: 'i' :: 'n' :: 'e' :: _) => 9 :: digits2 (tail xs)
-    (c :: cs) => let x = ord c in
-        case x < 58 of
-          True => case 48 < x of
-            True => x - 48 :: digits2 cs
-            False => digits2 cs
-          False => digits2 cs
-    Nil => Nil
-
-
-combine : List Int -> Int
-combine Nil = 0
-combine (x :: Nil) = x * 10 + x
-combine (x :: y :: Nil) = x * 10 + y
-combine (x :: y :: xs) = combine (x :: xs)
-
-part1 : String -> (String -> List Int) -> Int
-part1 text digits =
-  let lines = split (trim text) "\n" in
-  let nums = map combine $ map digits lines in
-  foldl _+_ 0 nums
-
-runFile : String -> IO Unit
-runFile fn = do
-  text <- readFile fn
-  putStrLn fn
-  putStrLn "part1"
-  putStrLn $ show (part1 text (digits1 ∘ unpack))
-  putStrLn "part2"
-  putStrLn $ show (part1 text (digits2 ∘ unpack))
-  putStrLn ""
-
-
--- Argument is a hack to keep it from running at startup.  Need to add IO
-main : IO Unit
-main = do
-  runFile "aoc2023/day1/eg.txt"
-  runFile "aoc2023/day1/eg2.txt"
-  runFile "aoc2023/day1/input.txt"
diff --git a/aoc2023/Day2.newt b/aoc2023/Day2.newt
deleted file mode 100644
index 79a812c..0000000
--- a/aoc2023/Day2.newt
+++ /dev/null
@@ -1,82 +0,0 @@
-module Day2
-
-import Prelude
-import Node
-
-Draw : U
-Draw = Int × Int × Int
-
-data Game : U where
-  MkGame : Int -> List Draw -> Game
-
--- Original had class and instance...
--- Add, Sub, Mul, Neg
-
-max : Int -> Int -> Int
-max x y = case x < y of
-  True => y
-  False => x
-
-pfunc repr : {a : U} -> a -> String := `(a,o) => ''+o`
-pfunc jrepr : {a : U} -> a -> String := `(a,o) => JSON.stringify(o, null, '  ')`
-pfunc toInt : String -> Int := `s => Number(s)`
-
-maxd : Draw -> Draw -> Draw
-maxd (a,b,c) (d,e,f) = (max a d, max b e, max c f)
-
-lte : Draw -> Draw -> Bool
-lte (a,b,c) (d,e,f) = a <= d && b <= e && c <= f
-
-parseColor : String -> Either String Draw
-parseColor line = case split line " " of
-  (n :: "red" :: Nil) => Right (toInt n,0,0)
-  (n :: "green" :: Nil) => Right (0,toInt n,0)
-  (n :: "blue" :: Nil) => Right (0,0,toInt n)
-  x => Left $ "Bad draw" ++ repr x
-
--- FIXME implicit isn't being solved in time here.
-parseDraw : String -> Either String Draw
-parseDraw line =
-  case mapM parseColor $ split line ", " of
-    Right parts => Right $ foldl maxd (0,0,0) parts
-    Left err => Left err
-
-parseGame : String -> Either String Game
-parseGame line =
-  let (a :: b :: Nil) = split line ": "
-    | _ => Left $ "No colon in " ++ line in
-  let ("Game" :: ns :: Nil) = split a " "
-    | _ => Left $ "No Game" in
-  let (Right parts) = mapM parseDraw $ split b "; "
-    | Left err => Left err in
-  Right $ MkGame (toInt ns) parts
-
-part1 : List Game -> Int
-part1 Nil = 0
-part1 (MkGame n parts :: rest) =
-  let total = foldl maxd (0,0,0) parts in
-  if lte total (12,13,14)
-    then n + part1 rest
-    else part1 rest
-
-part2 : List Game -> Int
-part2 Nil = 0
-part2 (MkGame n parts :: rest) =
-  let (a,b,c) = foldl maxd (0,0,0) parts
-   in a * b * c + part2 rest
-
-run : String -> IO Unit
-run fn = do
-  putStrLn fn
-  text <- readFile fn
-  let (Right games) = mapM {Either String} parseGame (split (trim text) "\n")
-    | Left err => putStrLn $ "fail " ++ err
-  putStrLn "part1"
-  printLn (part1 games)
-  putStrLn "part2"
-  printLn (part2 games)
-
-main : IO Unit
-main = do
-  run "aoc2023/day2/eg.txt"
-  run "aoc2023/day2/input.txt"
diff --git a/aoc2023/Day3.newt b/aoc2023/Day3.newt
deleted file mode 100644
index 652b04a..0000000
--- a/aoc2023/Day3.newt
+++ /dev/null
@@ -1,104 +0,0 @@
-module Day3
-
-import Prelude
-import Node
-import Aoc
-
-pfunc repr : {a : U} -> a -> String := `(a,o) => ''+o`
-pfunc jrepr : {a : U} -> a -> String := `(a,o) => JSON.stringify(o, null, '  ')`
-
-
-maybe : ∀ a b. b → (a → b) → Maybe a → b
-maybe def f Nothing = def
-maybe def f (Just a) = f a
-
--- was 'structure' I could make a `record` that destructures to this..
-data Number : U where
-  MkNumber : (start : Nat) -> (stop : Nat) → (value : Int) → Number
-
-
-numbers : List Char -> List Number
-numbers arr = go arr Z
-  where
-    go : List Char → Nat → List Number
-    go (c :: cs) start = if isDigit c
-      then case span isDigit (c :: cs) of
-          (front,back) => let stop = start + length front
-            in MkNumber start stop (stringToInt $ pack front) :: go back stop
-      else go cs (S start)
-    go Nil start = Nil
-
-
-range : ∀ a. Nat -> Nat -> List a -> List a
-range _ _ Nil = Nil
-range _ Z _ = Nil
-range Z (S k) (x :: xs) = x :: range Z k xs
-range (S n) (S m) (x :: xs) = range n m xs
-
-isPart : List (List Char) -> Nat -> Number -> Bool
-isPart rows row (MkNumber start end _) =
-  checkRow (pred row) || checkRow row || checkRow (S row)
-  where
-    isThing : Char -> Bool
-    isThing c = not (isDigit c || c == '.')
-
-    checkRow : Nat -> Bool
-    checkRow r = case getAt r rows of
-      Nothing => False
-      Just chars => case filter isThing (range (pred start) (S end) chars) of
-        Nil => False
-        _ => True
-
-getValue : Number -> Int
-getValue (MkNumber _ _ v) = v
-
-part1 : List (List Char) -> Int
-part1 rows =
-    foldl (\ acc num => acc + getValue num) 0 $
-      join $ map (partNums rows) $ enumerate rows
-  where
-    partNums : List (List Char) -> (Nat × List Char) -> List Number
-    partNums grid (r, cs) =
-      filter (isPart grid r) $ (numbers cs)
-
-gears : List (List Char) -> List Char -> Nat -> Int
-gears rows row y =
-    let a = numbers (getAt! (pred y) rows)
-        b = numbers (getAt! y rows)
-        c = numbers (getAt! (S y) rows)
-        all = a ++ b ++ c
-        cands = map fst $ filter (_==_ '*' ∘ snd) (enumerate row)
-    in foldl _+_ 0 $ map (check all) cands
-  where
-    ratio : List Int → Int
-    ratio (a :: b :: Nil) = a * b
-    ratio _ = 0
-
-    match : Nat → Number → Bool
-    match y (MkNumber start stop value) = pred start <= y && y < S stop
-
-    check : List Number → Nat →  Int
-    check nums y = ratio $ map getValue (filter (match y) nums)
-
-part2 : List (List Char) -> Int
-part2 rows =
-  foldl go 0 (enumerate rows)
-  where
-    go : Int → Nat × List Char → Int
-    go acc (y, row) = acc + gears rows row y
-
--- 4361 / 467835
--- 517021 / 81296995
-run : String -> IO Unit
-run fn = do
-  content <- readFile fn
-  let grid = (splitOn '\n' $ unpack $ trim content)
-  putStrLn fn
-  printLn (part1 grid)
-  printLn (part2 grid)
-
-main : IO Unit
-main = do
-  run "aoc2023/day3/eg.txt"
-  run "aoc2023/day3/input.txt"
-
diff --git a/aoc2023/Day4.newt b/aoc2023/Day4.newt
deleted file mode 100644
index 39fb721..0000000
--- a/aoc2023/Day4.newt
+++ /dev/null
@@ -1,63 +0,0 @@
-module Day4
-
-import Prelude
-import Node
-
-Round : U
-Round = List Int × List Int
-
-parseRound : String → Maybe Round
-parseRound s =
-  let (a :: b :: Nil) = split s ": "   | _ => Nothing in
-  let (l :: r :: Nil) = split b " | "  | _ => Nothing in
-  Just (nums l, nums r)
-  where
-    -- Nat or Int here?
-    nums : String → List Int
-    -- catch - split returns empty strings that become zeros
-    nums s = map stringToInt $ filter (_/=_ "") $ split (trim s) " "
-
-parse : String -> Maybe (List Round)
-parse s = mapM parseRound (split (trim s) "\n")
-
-pfunc pow : Int → Int → Int := `(x,y) => x ** y`
-
-part1 : List Round → Int
-part1 rounds = foldl _+_ 0 $ map score rounds
-  where
-    -- TODO we'll keep the math in Int land until we have magic Nat
-    score : Round → Int
-    score (a,b) = let count = natToInt $ length $ filter (\ n => elem n b) a
-      in if count == 0 then 0 else pow 2 (count - 1)
-
-part2 : List Round → Int
-part2 rounds = go 0 $ map (_,_ 1) rounds
-  where
-    mark : Int -> Nat → List (Int × Round) → List (Int × Round)
-    mark _ _ Nil = Nil
-    mark v Z rounds = rounds
-    mark v (S k) ((cnt, round) :: rounds) = (cnt + v, round) :: mark v k rounds
-
-    go : Int → List (Int × Round) → Int
-    go acc Nil = acc
-    go acc ((cnt, a, b) :: rounds) =
-      let n = length $ filter (\ n => elem n b) a
-      in go (acc + cnt) $ mark cnt n rounds
-
-run : String -> IO Unit
-run fn = do
-  putStrLn fn
-  text <- readFile fn
-  let (Just cards) = parse text
-    | _ => putStrLn "fail"
-  putStrLn "part1"
-  printLn (part1 cards)
-  putStrLn "part2"
-  printLn (part2 cards)
-
--- 13/30
--- 25004/14427616
-main : IO Unit
-main = do
-  run "aoc2023/day4/eg.txt"
-  run "aoc2023/day4/input.txt"
diff --git a/aoc2023/Day5.newt b/aoc2023/Day5.newt
deleted file mode 100644
index e69e99f..0000000
--- a/aoc2023/Day5.newt
+++ /dev/null
@@ -1,119 +0,0 @@
-module Day5
-
-import Prelude
-import Node
-import Aoc
-
--- AoC lib?
--- nums : String → List Int
--- nums s = map stringToInt $ filter (_/=_ "") $ split (trim s) " "
-
-data MapEntry : U where
-  -- dest / src / len
-  MkEntry : Int → Int → Int → MapEntry
-
-src : MapEntry -> Int
-src (MkEntry d s l) = s
-
-Map : U
-Map = List MapEntry
-
-data Problem : U where
-  MkProb : List Int → List Map → Problem
-
-parseEntry : String → Either String MapEntry
-parseEntry part = case nums part of
-  (dest :: src :: len :: Nil) => Right $ MkEntry dest src len
-  _ => Left $ "Bad part " ++ part
-
-parseMap : List String → Either String Map
-parseMap (_ :: parts) = mapM parseEntry parts
-parseMap x = Left $ "bad map " ++ debugStr x
-
-parseFile : String → Either String Problem
-parseFile content = do
-  let parts = split (trim content) "\n\n"
-  -- TODO deconstructing let
-  let (first :: rest) = parts
-    | _ => Left "expected some parts"
-  let (_ :: x :: Nil) = split first ": "
-    | _ => Left $ "expected ': ' in " ++ first
-
-  let seeds = nums x
-  maps <- mapA (λ part => parseMap (split part "\n")) rest
-  Right $ MkProb seeds maps
-
-applyEntry : Int → MapEntry → Int
-applyEntry n (MkEntry dest src len) =
-  if src <= n && n < src + len then n + dest - src else n
-
-applyMap : Int → Map → Int
-applyMap n Nil = n
-applyMap n (MkEntry dest src len :: es) =
-  if src <= n && n < src + len then n + dest - src else applyMap n es
-
-min : Int → Int → Int
-min x y = if x < y then x else y
-
-part1 : Problem → IO Unit
-part1 (MkProb seeds maps) = do
-  let loc = map (λ s => foldl applyMap s maps) seeds
-  let part1 = foldl min 999999999 loc
-  putStrLn $ "part1 " ++ show part1
-
-Range : U
-Range = Int × Int
-
-apply' : Range → List MapEntry → List Range
-apply' (r1, r2) x = case x of
-  Nil => (r1, r2) :: Nil
-  (MkEntry d s l) :: es =>
-    if r2 + r1 <= s then (r1,r2) :: Nil -- map after range
-    else if s + l <= r1 then apply' (r1, r2) es -- map before range
-    -- take off any bare range on front
-    else if r1 < s then
-      (r1, s - r1) :: apply' (s, r2 + r1 - s) x
-    else if s + l < r1 + r2 then
-      let slack = r1 - s in
-      (r1 + d - s, l - slack) :: apply' (r1 + l - slack, r2  + slack - l) x
-    else
-      (r1 + d - s, r2) :: Nil
-
-
-apply : List Range → List MapEntry → List Range
-apply ranges entries =
-  let entries = qsort (\ a b => src a < src b) entries in
-  join $ map (\ r => apply' r entries) ranges
-
-mkRanges : List Int → Maybe (List Range)
-mkRanges (a :: b :: rs) = do
-  rs <- mkRanges rs
-  Just $ (a,b) :: rs
-mkRanges Nil = Just Nil
-mkRanges _ = Nothing
-
-part2 : Problem → IO Unit
-part2 (MkProb seeds maps) = do
-  let (Just ranges) = mkRanges seeds
-    | Nothing => printLn "odd seeds!"
-  let results = foldl apply ranges maps
-  -- putStrLn $ debugStr results
-  let answer = foldl min 99999999 $ map fst results
-  putStrLn $ "part2 " ++ show answer
-
-run : String -> IO Unit
-run fn = do
-  putStrLn fn
-  text <- readFile fn
-  let (Right prob) = parseFile text
-    | Left err => putStrLn err
-  putStrLn $ debugStr prob
-  part1 prob
-  part2 prob
-
--- 35 / 46
--- 282277027 / 11554135
-main : IO Unit
-main = do
-  run "aoc2023/day5/eg.txt"
-  run "aoc2023/day5/input.txt"
diff --git a/aoc2023/Day6.newt b/aoc2023/Day6.newt
deleted file mode 100644
index 30b7b9a..0000000
--- a/aoc2023/Day6.newt
+++ /dev/null
@@ -1,74 +0,0 @@
-module Day6
-
-import Prelude
-import Node
-import Aoc
-
-Problem : U
-Problem = List (Int × Int)
-
-pNums : String → Either String (List Int)
-pNums line =
-  let (_ :: line :: Nil) = split line ": "
-    | _ => Left "expected two parts" in
-  Right $ nums line
-
-parse : String → Either String Problem
-parse content = do
-  let (a :: b :: Nil) = split (trim content) "\n"
-    | _ => Left "expected two lines"
-  times <- pNums a
-  dists <- pNums b
-  Right (zip times dists)
-
-part1 : Problem → Int
-part1 prob = go 1 prob
-  where
-    run : Int -> Int -> Int → Int → Int
-    run time dist t count =
-      let count = if dist < t * (time - t) then count + 1 else count in
-      if time == t then count
-      else run time dist (t + 1) count
-
-    go : Int → Problem → Int
-    go acc Nil = acc
-    go acc ((time,dist) :: prob) = go (acc * run time dist 0 0) prob
-
-part2 : Int × Int → IO Unit
-part2 (time,dist) = do
-  let t = intToDouble time
-  let d = intToDouble dist
-  let x = sqrtDouble (t * t - intToDouble 4 * d)
-  let start = (t - x) / intToDouble 2
-  let stop = (t + x) / intToDouble 2
-  let s = doubleToInt $ ceilDouble start
-  let e = doubleToInt $ ceilDouble stop
-  putStrLn $ "part2 " ++ show (e - s)
-
-parse2 : String → Either String (Int × Int)
-parse2 content =
-  let (a :: b :: Nil) = split (trim content) "\n"
-    | _ => Left "too many parts" in
-  let time = stringToInt $ pack $ filter isDigit $ unpack a
-      dist = stringToInt $ pack $ filter isDigit $ unpack b
-  in Right (time, dist)
-
-run : String -> IO Unit
-run fn = do
-  putStrLn fn
-  text <- readFile fn
-  let (Right prob) = parse text | Left err => putStrLn err
-  putStrLn $ debugStr prob
-  putStrLn $ "part1 " ++ show (part1 prob)
-  let (Right prob) = parse2 text | Left err => putStrLn err
-  part2 prob
-  -- debugLog prob
-  -- part2 prob
-
--- 288 / 71503
--- 1413720 / 30565288
-
-main : IO Unit
-main = do
-  run "aoc2023/day6/eg.txt"
-  run "aoc2023/day6/input.txt"
diff --git a/aoc2023/Lib.newt b/aoc2023/Lib.newt
deleted file mode 100644
index d2b61d9..0000000
--- a/aoc2023/Lib.newt
+++ /dev/null
@@ -1,162 +0,0 @@
-module Lib
-
--- Prelude
-data Unit : U where
-  MkUnit : Unit
-
-data Bool : U where
-  True : Bool
-  False : Bool
-
-data Nat : U where
-  Z : Nat
-  S : Nat -> Nat
-
-data Maybe : U -> U where
-  Just : {a : U} -> a -> Maybe a
-  Nothing : {a : U} -> Maybe a
-
-data Either : U -> U -> U where
-  Left : {a b : U} -> a -> Either a b
-  Right : {a b : U} -> b -> Either a b
-
-
-infixr 7 _::_
-data List : U -> U where
-  Nil : {a : U} -> List a
-  _::_ : {a : U} -> a -> List a -> List a
-
-Cons : {a : U} -> a -> List a -> List a
-Cons x xs = x :: xs
-
--- TODO where clauses
-reverse' : {A : U} -> List A -> List A -> List A
-reverse' Nil acc = acc
-reverse' (x :: xs) acc = reverse' xs (x :: acc)
-
-reverse : {A : U} -> List A -> List A
-reverse xs = reverse' xs Nil
-
-length : {a : U} -> List a -> Nat
-length Nil = Z
-length (x :: xs) = S (length xs)
-
-infixr 0 _,_
-
-data Pair : U -> U -> U where
-  _,_ : {a b : U} -> a -> b -> Pair a b
-
--- Idris says it special cases to deal with unification issues
-infixr 0 _$_
-
-_$_ : {a b : U} -> (a -> b) -> a -> b
-f $ a = f a
-
--- JS Bridge
-
-ptype Dummy
-
-
-ptype World
-data IO : U -> U where
-  MkIO : {a : U} -> (World -> Pair World a) -> IO a
-
--- TODO unified Number for now
-
-
-
-
-
-ptype Array : U -> U
-
-pfunc arrayToList : {a : U} -> Array a -> List a := "
-(a, arr) => {
-  let rval = Nil(a)
-  for (let i = arr.length - 1; i >= 0; i--) {
-    rval = Cons(a, arr[i], rval)
-  }
-  return rval
-}
-"
-
-pfunc listToArray : {a : U} -> List a -> Array a := "
-(a, l) => {
-  let rval = []
-  while (l.tag !== 'Nil') {
-    rval.push(l.h1)
-    l = l.h2
-  }
-  return rval
-}
-"
-pfunc alen : {a : U} -> Array a -> Int := `(a,arr) => arr.length`
-pfunc aget : {a : U} -> Array a -> Int -> a := `(a, arr, ix) => arr[ix]`
-pfunc aempty : {a : U} -> Unit -> Array a := `() => []`
-
-pfunc getArgs : List String := `arrayToList(String, process.argv)`
--- Maybe integrate promises?
-
-
-pfunc ord : Char -> Int := `(c) => c.charCodeAt(0)`
-
-pfunc _<_ : Int -> Int -> Bool := `(x,y) => (x < y) ? True : False`
-pfunc _<=_ : Int -> Int -> Bool := `(x,y) => (x <= y) ? True : False`
-pfunc _+_ : Int -> Int -> Int := `(x,y) => x + y`
-pfunc _-_ : Int -> Int -> Int := `(x,y) => x - y`
-pfunc _*_ : Int -> Int -> Int := `(x,y) => x * y`
-pfunc _/_ : Int -> Int -> Int := `(x,y) => x / y`
-
-infix 6 _<_ _<=_
-infixl 8 _+_ _-_
-infixl 9 _*_ _/_
-
--- Ideally we'd have newt write the arrows for us to keep things correct
--- We'd still have difficulty with callbacks...
-pfunc fs : Dummy := `require('fs')`
-pfunc readFile : (fn : String) -> String := `(fn) => fs.readFileSync(fn, 'utf8')`
-pfunc log : {a : U} -> a -> Dummy := `(a, obj) => console.log(obj)`
-
-pfunc p_strHead : (s : String) -> Char := `(s) => s[0]`
-pfunc p_strTail : (s : String) -> String := `(s) => s[0]`
-
-pfunc trim : String -> String := `s => s.trim()`
-pfunc split : String -> String -> List String := "(s, by) => {
-  let parts = s.split(by)
-  let rval = Nil(String)
-  parts.reverse()
-  parts.forEach(p => { rval = _$3A$3A_(List(String), p, rval) })
-  return rval
-}"
-
-pfunc slen : String -> Int := `s => s.length`
-pfunc sindex : String -> Int -> Char := `(s,i) => s[i]`
-
-
-infixl 7 _++_
-pfunc _++_ : String -> String -> String := `(a,b) => a + b`
-
-
-pfunc trace : {a : U} -> String -> a -> a := "(_, lab, a) => {
-  console.log(lab,a)
-  return a
-}"
-
-pfunc unpack : String -> List Char
-  := "(s) => {
-    let acc = Nil(Char)
-    for (let i = s.length - 1; 0 <= i; i--) acc = _$3A$3A_(Char, s[i], acc)
-    return acc
-}"
-
-foldl : {A B : U} -> (B -> A -> B) -> B -> List A -> B
-foldl f acc Nil = acc
-foldl f acc (x :: xs) = foldl f (f acc x) xs
-
-map : {A B : U} -> (A -> B) -> List A -> List B
-map f Nil = Nil
-map f (x :: xs) = f x :: map f xs
-
-
-infixl 9 _∘_
-_∘_ : {A B C : U} -> (B -> C) -> (A -> B) -> A -> C
-(f ∘ g) x = f (g x)
diff --git a/aoc2023/Node.newt b/aoc2023/Node.newt
deleted file mode 100644
index 98bcdb8..0000000
--- a/aoc2023/Node.newt
+++ /dev/null
@@ -1,7 +0,0 @@
-module Node
-
-import Prelude
-
-pfunc fs : JSObject := `require('fs')`
-pfunc getArgs : List String := `arrayToList(String, process.argv)`
-pfunc readFile uses (MkIORes) : (fn : String) -> IO String := `(fn) => (w) => Prelude_MkIORes(require('fs').readFileSync(fn, 'utf8'), w)`
diff --git a/aoc2023/Prelude.newt b/aoc2023/Prelude.newt
deleted file mode 120000
index bb92875..0000000
--- a/aoc2023/Prelude.newt
+++ /dev/null
@@ -1 +0,0 @@
-../src/Prelude.newt
\ No newline at end of file
diff --git a/aoc2023/README.md b/aoc2023/README.md
deleted file mode 100644
index c56658b..0000000
--- a/aoc2023/README.md
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Attempts to port AOC2023 solutions from Lean4 to see how usable newt is.
diff --git a/aoc2023/day1/eg.txt b/aoc2023/day1/eg.txt
deleted file mode 100644
index 4cba7d0..0000000
--- a/aoc2023/day1/eg.txt
+++ /dev/null
@@ -1,5 +0,0 @@
-1abc2
-pqr3stu8vwx
-a1b2c3d4e5f
-treb7uchet
-
diff --git a/aoc2023/day1/eg2.txt b/aoc2023/day1/eg2.txt
deleted file mode 100644
index 41aa89c..0000000
--- a/aoc2023/day1/eg2.txt
+++ /dev/null
@@ -1,7 +0,0 @@
-two1nine
-eightwothree
-abcone2threexyz
-xtwone3four
-4nineeightseven2
-zoneight234
-7pqrstsixteen
diff --git a/aoc2023/day1/input.txt b/aoc2023/day1/input.txt
deleted file mode 100644
index 495c9b2..0000000
--- a/aoc2023/day1/input.txt
+++ /dev/null
@@ -1,1000 +0,0 @@
-four82nine74
-hlpqrdh3
-eightsevenhrsseven988
-324pzonenine
-fglpbone79fourvrgcmgklbmthree
-fmbbkvthdcdmcjxzclk42six4
-four22xcqsnvktnpfshtmm
-qmfsccxsixfivelnmpjqjcsc1sixpfpmeight
-eight1nine5nine9six
-s4r91seven
-6pspkslrnxpplkhgqlcqfour
-sixeightnzrzgjvsrnmtqgx5
-sixtwo1
-h6
-five8pbcsllrbvg787
-dpfhfeight28onefourtwo
-vxqbtkxjtwoz3seven
-8ksrcjrcmpbq9rtvtvrbgljzqvbnxddnzt
-mpftpsgp6fourvdmltwojd9
-2fivetwosix
-3qqx2
-jsbdh16snnllpvvgnggfive5nhjpgdzh
-4fmgmmbonegtsnqfdqt1pm
-2onendvlmcrvzsnpr83nine
-8ninelfhkhnqtdfour
-8reight
-84gnprjhr3eightsixsix
-1nc7two
-3zcgkgrnd1d4
-nmfqfivervqkxmkdpnine51
-1fdtrptkb3
-nineone7kks
-ninelzgncpeight966427
-eightrsniner9
-nine7two4
-253slq
-lkhthreetwo982rrc
-fivegdsfnfour64sixtqfour
-dkfdtgnine9
-1six15ninebgnzhtbmlxpnrqoneightfhp
-32fivefivexjvckfourseven5seven
-onexxzvptxkn42eightvsdgszdjgp
-three6sevennine
-mvsrflqjsix22lhd2twodkltkmsk
-threetnbfsfxxhseven51cjvmkvzkdhr2
-11twoxjszm93
-trr62fivedvktlheight19
-4hxthreepqptvkkzmfsevenfourxeight
-5shqhrjtdgsninepblpjprtqptz
-ptwone9kzvjhhfive7qjsblztmfvthreeqrhhmbgjpqrgqhcgzntmvskhh
-xltqzgqxbkq7krgnthtqbm3636
-nvvxfxbgldrb2seven7twokxzbfkvptflnhlqjrthreeoneights
-7fcvckqszbj
-eight1ninethreeninenbmcsqtrl7
-zkqmlqmtszrbvnjnvsevennine9sevenqjrlxqjlql
-428
-8seven16nineeight
-24bkfzsrxjtbzbknqqxtfftzlnrkeight
-two372eightnine
-skxf5zpnmzqgvzjv9sixtwo
-1fivedsghrseven4
-8hmb75twotwo
-2hsnpfourthree3h88cz
-6qkqxszvghrdslpckhfivedlx
-pnxvtbflleightjpfzlqxhr22ckjrnzhnbvdnj1xnfhmb
-cdscn4xksngscvnseven
-65oneightpln
-ninesix11six41seven5twonesl
-f411d
-sixonedqppgfdfbthree1sj1sevenqhdjlg
-eightsixhzshtg5oneone
-tbhdgzphkkvbbclmhgvb3three
-dpsxdfmzstpd7rzf3
-kzpctbr3oneninevgcxcvsconeightgk
-blmpjv6ltxfqsqfjnjgxtseven82
-99four
-onexsxs3sixdnfqlffjnnrfive
-4sevenzdjvrqjlx33
-brtbqvzcdtlkn83sevenmmtwo
-5bnlmjtmeight
-twotwofive2fqbfvqhp65eight
-dstwoneninekfourphth4lrfjjrh
-mqsndqcxt3
-5mbfxskgnh1twoqbxfbcjkzf
-6fourzdcmdl78pvxxjrplmtmvhh
-3mzgttvpt8gvzoneseven21
-8253fgfhpmponef8
-nineninelhntskjvd25
-1czbccmrlch27three
-one4l5four
-sixmcnsxf5two
-onethree2five7vzhctscktrcx
-14szp5fqtqfzcd
-6cgpzjprtsjd8five4vjzfhgkbbf9
-7gt
-4lzx
-fonexgjsnine8
-1twomvdvdrrneight8fivenine
-59eightthreesevenctwon5
-2dxfivenqflqppm3bmtmblbkltwomc
-36mplfgblgff6
-threeseven8gf9sevennine85
-hfssbghbnonesvdm7onekssjbthxjjvnqmcgmrcx
-eightfrbrstlh8
-eight34sevendlhvhszcnvdlvctkdzsgq
-seven2eightmtsmflrx2three44rsk
-fg6
-mbf44
-5926386nine
-48vqvcffsq2eight7zktszfour
-djstrfnqsixone8oneightc
-5seventwoqtr3eight5
-dttwo88three
-8rdxmnrtmt
-r2tzcbr867onetwo
-2v489four2
-vsmfszr5
-84nxrm48
-5cp4five51three
-four3six3
-4zglqmdngeight1sqb
-3twosrlvbzfh6nkrhmnjqeightseven
-eightgjhs276five
-j15one683
-hnnonefvhnxggtwoz2five
-threeseven2fourkltqmthree
-bmksn4
-11ntrt
-5tctbxqjcngdhffqqrjfive
-vcstnf1
-98tgzlvtwobjpxj6
-one6j5hqgbvhtmsjkbt7mglhvjjxmtwo
-1sixq
-three8lbqdd38ljfourtwoccntjgnmv
-two5msdsntdrjl4six15tdpnknrxnine
-sevenzkbfmqxb2sixsevenbvnbxtxvfournine
-1nzdfninednkhghlscsc
-onefive3gvjsqqgx7seventhree
-8dglgts4slg5sixninevzsj
-dxdmkshgssevenfour967ninetwo
-4ninevrhsbqnjtwo
-358fiveseven
-two8sixzt2
-93ninefztjqrhdlxxsjnnflczbsjqpkrmsixtngxqk
-ltpnkxtwoeightcfpjhthree5brzhffour
-four3five6q645qxn
-fourjxqghk6
-8dznl428nine
-1djftqndtmkcbptxs22
-27one
-543
-qgtbvgnl4tzfgch7zqtmpsix
-fourxfgqcsgxbg741922nine
-two4sixmkvkftwo5one
-lrlnnbdzr82g58fkgvfninezmqv
-2xbkhjbrlztnphmcsfcln
-2xlxksqkb
-rcnzsrtfive9scnnvqx6kmkvgmxlpqtkmbjtvsfmvseven
-6oneninekfpnbngn2
-2nnxlthmxqc9eighttcznxdchdthree
-dznqtbkgtwo5zpthvsnone
-7nxjjzhfhpshccknpbpttrjhqkxmmssvtlxtmbxlhvtjczone5twonecf
-96eight
-7qvckkdtvzjd
-14nine1two
-eight87one8ncdzkptqrgtfclsevenc
-8fourfive
-jjqbpmp42589stwosix
-vtrbqpv9sevenone1qlvmzkthnnsevenseven
-pxnxptttxh6fourmbpcldrlfnjtcxtwoonefour
-8njghfrsix82
-gvns197fsgtwo
-9sljnsix8
-rnine7ninethreenjxnrqgzbxbtvrltbss
-4stzbqg44f
-3ninesevennvvdmgkxzmttcxfbsvjrg
-eightsix3twofmnvs
-one2fmzxnhhrnvlttxnhbrjsgjsqkvfn5
-qz9ptnxfngfrh65bvvbhtsrsntczgj
-qfvqfpb2txnxxd2fiventvznljcqj
-fiveqvmzqlgzdbvqzjbllzeight5bgt
-qggflvv753clcqqjqmngdm6onefour
-3fourfiveeightbbgcgtwo857
-one5nineeightg44
-6zmqxcl16twofivedjxhzmhffive
-jnnsixsixtwo2bgsnbrzlnlltb
-six63oneightgdg
-pftmhdnqdgfive1three42four
-8hkcjlskh82
-84
-1ninefour9sxmppxjqqxpn
-ndrgrhsp1gxcrfgxctv
-fiverzmcmbqd78gqm
-fiveeight4
-vxktmrcdlsfiveoneftvqnnvjfour8sixlmldnrceight
-hpfprllctdjtwo9ksszn8eightcfdbzz
-nine5fourfbgf8one7t
-8sqxm5
-6fxcxhn
-2prktdcvnine1
-2vqrlpffvjlfourktdhxxgvonedvnsvlld
-qk7294fl
-sevenfivesevensevensn4
-rnpqmrgczhllzszvkfzmcljzpthree8
-fdcqknlctq74
-1xnvpvfgsbslkkktxxhn
-one5eight3zrldkdj
-nlvgbz71fourk33
-sixfourfour6three2three
-7lszpqqq795nzdfxbzsqlsix
-one8nkqdtctsjj
-7xfphzjzndr1
-keightwo25hmqthbeight
-2sixdm
-l4eight1fourfour
-2ldzseven3eightmdmsgkrrfivetwobbzz
-mtwoneonezdfour22two6
-7fnjbjqdxvkntlfkhkvnzt
-dhqsqnslccxgdd63x
-nine6fourthree
-7qzbrpplm9
-pqbdbxxxggn9fivebfttnine
-58h152eightjmjqlzjjp
-8vjrtblqzsx
-7sevenonesevenhqkvxxsvrsix
-four6hcxdtwozjnpsdtpzxxninevzvsxffxpctcjbtmlm
-3xznljnjz4ms3seven
-8892
-3jrzlmpnxhfivefivetwoseven7
-onethreetjpmpvpr6threethreeone
-one5thcfourndbphpxszjmt7eightwof
-r5s
-fmjzjqlnhxqhvbdvdfbdnb4
-nine9mrqdgnkc
-nm5jxpjgsm31stkvxjseven5
-hplgpfrtlb8dgsbbljfdgknfvqbonexbcddflz
-4bmfrjvj81vvnztchfrjfive
-xvvb2nfqxdmpzjvrbmvvtmc16
-txrfivecjq6hlgjbvzp3threefourone
-sixlthreeeightn9hqmxhxfjrb15
-six6eightone3
-9six7
-nineoneseven2eightbr5nine
-sixqqdsdmtkgkfq9
-3fivefiveffive
-8eightfive2six
-7rnlhrhlfive
-kvkrxgkk6one2ninermqtpbbnmpdpjxc
-nhltwonesix3five3two45sixk
-eightsmjnzfzjk8
-sixhxsprkfour5b9
-vkvhvhrvbnvz7rg944
-ccvzjppvjtthreetwoqdc4eight
-threefive9qlg3hkhvrbdxzdthree11
-onesevenczvffoureight28
-three39jddkzzjninetwo5
-63nine3sixlqnbtrq7jctmgdmk
-zxsqngxxfd9rvjjt14978five
-9983eight
-sevenddfpzjp3skz
-bzdpg73eight71ppzkeight3
-onevphctjs4
-twofive2jxsthree8sixqeightwozrv
-6klpdhhsdng
-thxtwonefive57rpseven2
-qtcdgdfj77sixrhtczdcbp3
-seventhree47
-threekjqqht883
-two3jfgsdnqbxcbzjtteight
-5zcpgcgsixdskfszmmq9hxtknineqmhg8
-snjs1lxkpbk5
-seventwo7bknk9
-rstbvlzlk1tpqjsjmhgdcvpfdqzl2bcbtn
-3eight4six2
-twonine8xkqp3eightgheightxplcqbvppj
-ninevkrvzvseven6eightcmmvgzb
-77n7fourthreecrcq
-xlvszfhhffhmvxfour8skpvl
-9nine3kfhgngkd1
-sevenfivesxdxhtkmeight4
-28four92
-mjzm465qffive9
-dqlghfxbkfourfivegfkmgmdgzxtm1
-six13lrc
-8qbvnhbplbl6
-13lmgbfsgnxone1
-ttdznnjsgjtwo5
-eightfourtwotwoltjxfourone3
-8threethreeeighthbbxfbmpj611
-ninekpjcrvlqbmsixseven5four
-8jmgspsevenfour7
-6nineone5hthbrbsjrhbnn2
-ninezzdlfiveseven4
-fhrxvsevenlvnztq4one
-cvmlmzz8njtfztfzfoneonejbckeight6
-ninexdgtgjjnrb1hrhjvchm
-63gqjvjtmzgkpbfthreesix
-fkstfchxcbrkfivemzhfdhsffd4mnbbmgprxcgmsl
-87rslqkvbzncfxddt
-7fiveeightxqjhdkbbgdjksn
-four375
-sixftdrnbzq84688three
-eightseven8kqdcbgtmvlsvxx24fqrfp
-four7vprrmq91
-six85ndzvnplxhkmrjftsixeight
-5twofourzfdxbffive
-4jbvmpnqcpbdfrkzone9ndcxtgsfive
-nine3jzpsrhb
-nine6cpqsfour
-78kzczxbcthreesixxtdkflhzfour5
-14sixsevennzgfnmppnmcddd9six
-fourncvgmhfl2fivefnlndmj
-rzgqvdgksz6six
-23seven2rhlv5
-9xlnnvnvccj
-3fivethreembplpfdjnineseven2
-jk1
-3threevgklhnnnccrmone2
-threefourfive4
-qtpbdrsix67threekslkmqt
-five3ghvqnrhtbqnvtmdlnine
-84lvnfx9nine
-nine7onethree46
-vtshvtcch5kxkzgkfourrtmbq
-5czsbzl3threeeighttwo
-38nine
-twovcxn9sixklflgptlkt
-fcjpjrxdleight87
-cfn6
-sixfourtpzpnsvghlqp3ssptlls
-trsjxmzvhxgvtzrhxqbb66nfp1knf
-twosevenmdmmcjjgxj96qxrqqteight
-sfcpfs9dpkvxrmjfiveseven
-6dblskzfsrpcnszqtwo9rgrdkjshb5three
-5fourfsblzr3onesix
-gcxsc9
-txjtwone12
-twovpgthxxrpsevenqxpmlbrr3three5
-csqkgmzl93xrxjs64gptsix
-33qjjzgjtrsflgpr6
-twoeightseven6zdtdltvzsxvlgsevensixpmxlfrb
-gjnvdxbveightone8two
-24vjdfhninezfvlgrdvsh8
-ninehn1685nineone
-twoonegsix4threeninezrsnvrltqlms
-5cdfdldjxddrjhncxtsndl8
-1mqg3nspfxnkfoursix9nine
-1tfcrfpqmk1stfrrnrz
-721dgsmsixjtxcxmj4jhkdsfj
-9plbxnrnlgsvtshfgzbkfive5qfbzgrxzk
-fourgjdt2
-ninethreeqqxrjjgskm1fourseven6
-rbrr1
-threekrslrrqngjtwo6
-llkbxgqp2cmnmgdfgrcshlmseightgjzs
-66sixeightthree
-64vdnrrqfxonespgfhzdcdrbrqone
-threervnhkgdg7oneeight
-nkbrvsvlzkonermsvxh65dlvxbxvlnq8
-twozbkclqppd9txxzbvfppz3
-two9nine
-7vnlqfgxlmninek2two
-qjzggvqj1ninefourrc2szbmczr
-seven6kfkkm7
-nqlgfzmdfsevenshvcnxdjvxveightfour9
-seventdrqkrxkeight75qjfbb44
-four3cxhlvthree3tcvrzk
-six5seven2
-3ninehcsjfstwo5xsgmkz6
-3fourlnthree1fourseven
-lsxzsskbsqmeightcrddxvxk93fivevfshztv
-nxqxrsevenl3eight
-239fourjcrffkeightfivezmfsvqvpz2
-hprcp6
-rklbzvhll4nstdjb7fourthreeonefour
-9jlnthv
-65six4dvtftwo
-nine5five3kqvrs183
-sixrgtckzc7nmczdx8three2
-4six61pzjhnhpbnmsq
-1fivembsixsevenddmrlkfour1
-qhgxrbnfc8one2vxc
-rdsttzt1sixonefive
-lsdoneight5pmlztbkvzffourfour7
-7g3
-3sevenlnjfvms9two
-dclkonefour5
-tskeightwo9one25ddmdmkqrpffoureight2
-rmkqgbh1slrtshgkgbdsftvbgm4
-qkhxmpfzf51
-648
-three4gfnxzrs2
-hmcskdltfourllp7sixfiveszgnfbpjt
-hf27ninep1fqdbglxngkf7
-seven6bfhtdztzvqhqnj2xfxchxpfc9
-8vfksvbfive9lxjhcfive
-626txvseventwo
-1bgzkmzx1
-nineeightlzv2l
-8ninetwo68twohhntdvjpzfone
-jsjfive535fdfnj3
-fnzrsevenhcgzccslt92twonine71
-4twothreemx
-6vbtgjssfoneqpsrdfrbcgmrfckfourpzdlb
-91svfsxrseight
-nzmnpbdqjdh2four
-blqjhjxplrxsevenonefive13
-fivef11gtdpgbdrxnbtrfqxfb7r
-l5fivethreenine
-oneffcdpqmvpcdcn6six944
-4mmfjltf7
-29threenine26
-8zrthtv56
-c21hxksz
-nqcbjkb7
-fourxtkrn7bvpbqtcg78
-qjvmvzbkxlseven756
-6g31dk1mnsgxhbdvndjgvsjr
-73eight
-61jlzgrrpkvgdpjzbbqkxp
-3368nineeightwodzl
-9tlqcrxsix7
-cmrrnf8five1
-4three72
-hhcghmtvznine6nineseventwo
-22tvjnfvzshdtpxzxrnzvtwo
-8threeqlkxrkfsevenfivegxmbhqg
-5mzzsldbk7ninefourjfjv
-rloneightcjhxsstwotwombktzlkdxtwo8
-three92nine1sixeightwof
-drxgb14twoone
-7one7seven258nineoneighthkd
-4four4sixninem
-fivejkjpdbfpsttjnpkv4one8phckjllc
-5bmeighteightgkjfkjthree
-98lkzpdnvs7chnmkxzql
-twosix2two15xzkpmctwo
-951
-four481six
-3tdvlonefiveone
-88fourgktxksmhninecfpljsix
-cphlzlx45fourxjphtthree
-6eight4gfjjdvslqv1six1kxlmn2eightwof
-5vxrzxgdpg7vrsrxrrhncfour
-5threethreemrzfbjq
-ninecsg9lseven828bjttzx
-5kqnine
-fivetdhxq39
-rcvlsix6pqzsggz59
-47fnrs
-724onesixtwo
-tdbb7
-sevenseven4
-two7mlzgdqthree
-2gxzbnlrglnvmqmzbznfngxfeightnrcrqsjnftfourone
-fivetwovsbvrfour2ndmltmprsqkbbztwo
-j3twoc6mmzt
-six47nine6tkpjleightwopzf
-sevenmshrczkdqfiverkmhlqjzqqhgppbsm58
-pkbgvlvzckvone26rfqbmtwo6
-sr9qsxjnine9zbc6three
-eight4qxlmtwo27threesix6
-fourone417oneone
-6fpvfbrrtwoeight
-79rj4eight88
-6vhfivevrj
-7tmqhchfive6jxgmqcfmq59eight
-threeone3xqcrjzszhseven2csbflgnds
-1qsxxxmsknhseven3nine
-fivemqxjlggcnsngflb5qtshllseven1onefive
-7476qfcmqqbfhvrvksfztskmzgvjjsrsc
-twosxlbrgdtptwo16
-kffmtjnjjk2fourtgv6rvsrzcvdrklplndseven
-eightzhrfgpjfqgccn2khrfdzfour28
-ninetwoxvnhfdjsxslone4four
-92nine48b
-ptwonefourclthree56
-hshqjfknineeightlkdxvxcsljfptlbb6kt
-fxjbr1four
-nine36gqbt6
-nsbcvzninebvlpvlx1three
-1ltlxzlmzxhjlfvtnrrpdk
-3jpqgspseven5qm
-553npbeightxf
-fourbspjfbxk4
-238
-xjrsdsvgncxddpmj3tlqone89
-68bkvsslntwo
-dxcmpjfprnthree98sbh
-reightwoeightseven76xqfhvbkfouronegkrfvdzzdx
-9lfpjff
-gcvs5
-hnctpgpxdlvklfsdfour2hnvtklhgqxhjpzknine
-ceightwoninefivetwo9plndfive4
-pjnzdrhtddjgllbf9f25eightb
-fpsdpfl8cnhkjtzhfbhdftkvm
-3cqqkflmjmpfmkk79lvkjljd71
-bfpfmkjpnkgspsz7nine
-threethreetmpntmpg3lfzzsrzr36plfvxv
-nvssix83
-dznrcvvgb8
-csrffxrtvmpfgbkcmmdlzxneightzvfgxdpljpcnrcn5
-9sixtxxthree
-seveneight2kpzpvvtzq8
-jbmmeighttwo12seven96bcvcs
-b68pvjcsnine8
-4vphtk7
-mxmjvnbqseven2
-3two2foureightxvvtxpcdmsdzvkg2mthmx
-cxslpdtnnx5five65
-97mp3qbkxmhl5dkphzgmpg5
-7f11sixcnrqone
-8fxjdjxc6drjxnhptdeightseven1six
-sixffvgcsfourhmnrf8
-qtpjrmlgnlkbbbr7sjcpm91five3
-5pqv69one
-eightnine8
-1three8
-39cspknxbsjhtfourpcbqsvlgz
-5nine15
-zgjgjfcdphnqqv4eightsixsevenkv
-6ggfxblx47nine2onenine
-1twoone2xfxfcr5
-sjvpxd7ncpclnc57one1
-4sixdgone
-89ptctqvnpg
-threefour1four4
-8seven5pfeightfive8hclpxjgftc3
-mznfsbmdtltwoqlf9
-425
-n51891
-one5l
-8ninefive2jhhbnjsvdqtlmsjgshvlvlh
-58ggdlkpcmkgeight2vcprcttwo
-twoseven3eightfivesevend
-krrzfivexrmvdtbr1zvqpmthreeonenqnmx
-2sixhjpxptnthreezkfsix
-jchkkkgrdmkvdgksevensevenfour8five6
-1tzbzthree
-xkone7zvgtv5qvln
-6fivetwohjblzsixnine
-onelpgkpggl9nsdxtgh4tgjfgpcsn3
-bjdxc7krrt16xbgvl
-sevenrpftshchmkkflxseven4eightsix
-groneightfftfvk6
-hrcshqtxpqgxeightsix1xxxrczpcr
-foureightthree9sdffivebdtrng
-ninefourthree9eighttwonine7xjrsm
-fivefour64
-51onefivetkcdbbslzmeighttwo8
-4rssgjpzgnczqtdrfivesix7bjxslhzthreefive
-5kgkv7ninethree
-84ninepsbvzkgrvqpzmtqgmcxpvgfbffns
-fourrvdzsntddfoursevenqq54lgdrtdcq
-4nineeightfdh
-9twoonefour2kmnb9
-qcvmnq13tsptksgmqj8
-113twonine4zjsbtjkpbdsix
-sevencvnineq6jvnshmg
-pjhmbnjqflvp452sevenfive69
-2three1sixninekmfcsbsevenfive3oneightg
-six3six62onevrhtsskzrhtthree
-5bxcmdnrf1szdgfournine
-fourxdxmk6
-3lsnfgffnlrqboneeight
-9sfsv4gqhpbqg86
-two17567fournqkmh
-7threesevenzgxvkhf
-vlmz7sevenfourfour8bqzdrdktklfivefq
-xxsvcqqeight6flrffzxpfourkzfstj9
-fourlzpdxg3knxgl
-msb246fourlc1crhlbjgdgr6
-1q1cmrmqponeightd
-twoeightncz513
-nine1nine
-8sixonesixnine
-193sixthree2rgthk
-tvhqp44hmjhzvmhgrbprgttgrt
-52bdszlvsvgzonefiveeight
-sdxnpkllmnninethree5jxsgkdbmknfrfvthree2
-six23hdzmppf67threeseven
-eight5nine76vbggdlp
-4onevrxnnbszk
-9ninezhdsfbfive12
-sixnine5xqmkmthz
-fiveskklnrr13sevenfour3nqs1
-sixqcxqnjxxzqmdlqtwo83
-8eight7
-9psvqdzpchr
-492jseven1
-xrccslcthreetsnfoursixsixsix1
-gskqmvnclfgxbtcq9hsix
-5two4twofive
-sqqhrvtszzjs1vfskhsdsvvhlskn
-nineseveneightcjcgnb9three3xfkst8
-ktwone4one73
-five6xncdddspkcbgklzlzn687
-xgnlvnskgklcpdqvks2
-zscmhb7mrrshccm
-five8hplscnineeight
-2hrgc86dsgjbvsrv9
-8lncmqrxcnm9ctpxjxlz8
-jdqt39336
-1gntnqbstzrnine5cqlrrtfllb13kfleight
-3jscjlvvkd89
-5nineseven66nine6twoonetwonek
-sevenxrqj4bfivesix1
-8msix8
-six6ninesevenfourbttvtt66
-4cmvvdfdgqphjzleight
-55mltlnxc4dmcrhjsjc8seven
-26197jtlvpsixcmzkslvzh
-rjzn2
-krlvgxone54hdddkspmfkpnzcbtbz
-four2two2
-one5vjjs3one6six
-6cmt88three
-reightwo7lrjqxbmgjj3seven2
-ntrkndgqzpfkjrone9
-5dvktjpseightxxmbtrm
-four6seven9936six7
-fourhqstnjbbdscjngp5fpxmg
-77five
-qrzg9five1qqcsonekgvckmmpfx6mpxd
-qzjqstcll7donekkpmkgpdthkjclrpth
-14seven
-bpbfnnq4rpppcjfeightsfcsqzg
-2one7eighttwo2vhzhjpgg9xhsdvlgxf
-eightonepn38ztcqzbthjz8
-lnsix7eightskqhrbx
-sixvnpkpsdzsbjgjkbxreight8five4
-vfrvkmnvnhk5one
-eight9nine7
-oneone5
-7584zprfmjtwo1
-4szpqtwoflcr9bhtthreeeight5
-385
-ninekdqknptxhsevenmrmjzqjvnppsrgbkv9jeight7
-5fs1sixeightthree
-sevenxkvxzqhckfourninetwo3eight
-9eightgfjvv
-xh8
-brbs3fiverzrtwo4jtdsvrljxone
-qcvfnlvfivetwofourgsdlcmkb5
-klnsqmblkffsq4threetwo6
-nine4eightx8eightwohrk
-c1
-sevennine55eightttlbshbfive3
-6ssmtjnxsixthreengrlndcb3
-vgpq8sixsix
-96xhrnine9
-grpsjz1zqzthreeone2four
-r6twosevenrdmczdz
-jdjz4ninefour
-one88
-ninerzdfc8rxnfbpndznctqd4tlb
-cshoneightnbdfmpdh2fnvjtxtshseven
-gtpljthree1six
-63eightfournncq
-twoonegsdpfkfqdf7
-xccnnscfivexbqmxfouroneeightgvndxgnine3
-mktvsff76bfqkq9fivetwo8lv
-3four5
-qhdgmcninethreevssbxqbsd35
-one6mprksdcz6hpxhrdznfpkmp
-six55ninernnmmlgmblttbgph8pqrjtjhtdj
-jnpbmnbqonemjcsgbg1
-9eightfourmkknzgmqh7two
-7five9
-2eight44skdlfbhfsshpvhgfseven
-2cqrzrhbfn
-three8419two7
-rvpblkzgkmxkghsbfn3one
-nine58
-74spkcfzsdmkf2six1
-2threeseven
-sf84qnthree5bmxnrmqff3seven
-oneonecxxv96
-gpdbgxgjqzdzlxgqphdr63twofourkspvxmvrfx
-fivesflg9fivesixonexfb1
-8pc56fourqpqmfour2eight
-3qvgqqldcr8
-tssixfourlbqstcmj1
-pf2sixpzxcpmxtp7twoseven
-5429
-drtlhzlqltwosevenfivetwo29
-eightlqtfronebqhdh1nineonembxnbpgg
-vlvnzcpbpqeightjspbbqqeight6
-sixkkmgcnhdfldplzk3five
-93ninekcmgjm8ckqjdz
-3dmskrqjd9
-five5threefivesix
-lgvbpdnp8oneeight7eight
-seven37
-2onesixtgbqbnn9eight
-5ndhfjrvt5fivetrhzsmqtwo
-bdcrhzdr33ninefive9
-cgsdzcninetwofive6one
-fiveljbtcqcqdglvjnd8onefour
-two2b5lzbjsqx7
-three593sevenfivetwovptpnmxffrkbsp
-sixonesixthree8btmzlnkvxt
-2jf59
-eightfivethreenine57qpdkcfr
-eightsix31threeeight512
-fourseven2twoninenineeightone
-pqtnqdtsix1
-3zpnvhlsjcmcdvzzlqp5
-sixvnmhckrzxfmjglc964nine
-mftxdnhdzmfnrgvvz59nlhhvr7spjrh
-eightls148mmvsjjldzlmvxjd
-3five5mlfhszsevensixthree
-4zpllkssevenfourtgbhdkltwoc
-ffourhnjhmtxxfjg511
-63jddsfqsmjdmgxnthree3four
-eight3onetwotwo7
-fmfour9tvfourfourtwonef
-qseven91two2fgnzcjnm
-rpzmsseven1jcxvxgnvthreeeight
-onefourrflrntpkskseven1kthreetwo
-5lpmhn1six
-ttvdgvf67btpqbslt
-3twovkbrhqsmv2lzggdlbfvgonenine
-rstknqvqtwo55sixjpzmgjsm
-nkgfnrxzj7jszsixfiveeightsixfourflqlzmhl
-sevenbbbmdgbv9oneightqg
-mzmksix42oneonexxmndklncn3bqj
-3xxcsfonefour
-1threeeightnine46zzscxblntplpd
-6four77sneight
-pcjxrxtwoseven71threethree
-5spmqztljvbtthreefivenineonesl
-6zlkxrbhlgf6
-228
-2seventhreesixfoursrhxxrcd
-vhkkr33
-twokzcchqdmpf3
-qrz9
-8lfkxtknx
-76n
-dpxthreeqgtjsqs33pzjxgrmtck
-1xhhdhqv6sixlcgfour
-four9chmvmrqmfq
-one5cvxtvjc96three3
-one6eight
-sevenxdncpgzqqv6five9
-fnlrctrph4mpdninetwo4threedm
-one3nine5two
-8prrdscmtgfivecsnxjrpssix56
-foursclkcvrkvkhrbnnchlsbllfive6djnprhmkxfnine
-five2twojknineddzszxsgxxgzfour
-9532chktx5
-two47
-42sscxflsevenjssjmzn3xgzpvfsneight
-7fltzgtkmqkgjj
-1one5six
-6gstggspddlninezrzcl5eightqdvjlgz
-eight2stxftmtsbn
-vqpqvbjvgklxrtvnkgsvlljgxlpxthkeight8fp
-sixpjhzscgthree8eight
-vgxfxhssbsixfivehxllx9
-nrszzljfrthree8
-dvthfklrvtworxtvhljnsqnbcnpj5eight53
-76threeqclnine
-eightvdc7one2four
-46five1threeeight3six
-five52k557sixxctdrb
-hk2twoggmfchleightxnshxrcvncbxvrzhone7
-21rpnnttwo4fivefivedvtpfmnbmg
-onetkgkv14sixdjfznpdrvl
-onezctthreemfnqcczxpffz2six5
-kzeightwovrtjp94vhn9mjlrxqm9xdzbvgqfqt
-34one17hl
-9332r
-zeightwottpsrgnljcmnglbfsxdkgffrlgm6jnzvkxn9
-pmzdljpgsix7
-zmhxkpskqzgrkptwofour4
-pkoneightsix7
-9695tfivexmspcgz
-ninerrlfckbs7vcmbhkninelbhfclninesevenbppk
-78k2qhvkzgkgkskhfiveone8
-ndxnqczhlkdvd97threeseven
-jmmdfvftbeightone8eight1twosevenseven
-five9six98grthvvqdjbrkxn1
-4qxvqfrkgnfcxkkdm1mnczs
-n3b
-three9bzfour57
-8threexkglxf2
-onedxfivedxvgxjmzkone3kbmplxbkdnpknjzrbmt
-nine3two9fivefrmjgxkrtrmzh
-tlgpkzfdlnine9fivezdl
-9fourtsnhlf5ljxrhflckjrrzfjbndhlcbv
-3tthree6zqrhbpqczsixrgvlcpm5
-twosixnzqtvhhnm8
-five6one6
-4fournine946nine7
-one8rzlnlcvdseven4seven
-tnmkgnbrzg5nmlqsevenone7oneeight
-eight985sjrfjdhtkrbd
-4threexlm6twoone5mthree
-four8fiveghddxqlp
-1kjtrpktpkq
-2grqpqfsclsgdzmkglxbzxcshrs811one
-9seven94ffkfdmvxr
-8tvnnbpj7bjmvlnnj
-sixthreeflggjxmlk54
-6five6ninecjdmkggsixnine
-sfjlhbbx6onexxjsix4z
-9bbnhtpgbntzlxct85
-2bltznvqgs8sixsix
-nms7vst8
-eight9vnrqbv
-two663
-1h6prckcqdqn
-2ninesevensixtwogkvtjrp6rbgc
-sbsncmpsixhfvttwo27fsb
-fourtwoshvjffjdeight83knlxbdjphsn
-bkbhjcgkjbcgjsix1
-cfkpjctlnztlsgjonehrmvtl7vksr
-8eightphhd
-6eighttwosix5one
-8dtnqgtrddjfqmlrptphfxkcgoneeight7
-32eightjfgtqjllmxtf6s
-twovqnctjcvsdfjbhtnzccd2gshchnhrpx
-twovqqpbrf9
-four4onelkjf15psdspgvvdfcvmnkhmfive
-xdpg4ninetsbrmpqfive
-fiveonefive19
-46qtppz
-twoseveneighteight72
-fivefourthreesevenbxtpqctslbkeight2qmvgth
-355ncxjffxt
-eight4zslht5six
-sdnsrghmbxxjhjqd1njqjcghsspmggzd2
-vcthxnqqkvqsjrkxrs71onetwo
-fivexcjvm9
-3kddthreehfhjmq9ninesix6
-rclqzddvxtm2nineninethreefour
-vlfgxbkdgnxrsprd386onethreetwo
-5sixjscbvzkxtl5fourone
-317dnqnqntwo65jnthjbxnfive
-mxtwonethreetwo2ninefour35lnhczqfpt4
-nlctnjrr9twopthreefmxgjeightwofqh
-nz8threefourbhcjvssgcnine
-sevensixzspvzjseven9
-six6onetwocnvmjfour4eightone
-7xfd5qlmtzhhgr
-8twonesch
-nineqvlsrfpdn2
-ptrfgdnine7gpxsix
-pfx4sixfoursix4fivesix
-68lqzp
-nine53jmtsxjptgmzpfoureight31
-two1msjf8
-gpgrpptthreetwomfrmkszrv8
-3five4
-threelqgs2kjvlsbmjkf
-4fourzgqkfhqhvhpgfkt
-jnlbcbgrp7
-onecdcmbrqxxlpbd1rthree
-99mbfdcgbhv
-nine6cvmfourfivesixhcsqfpxkdk
-eighthjbqsbz6ndpkdlnpmpxqvpmsrbvksnnleightnzxmjg
-gvvpnfzbb7zxfschnrteight6two5tnp
-sixrctqxdpkxpfdkglvthreenine47rzs
-jtwonefour8rkmtclhlf97fqpjmggtztwo
-slmfjkfgbjt6
-8lbh
-eightnqtfvvm2
-vseven31
-one54qrnzfrbdqfive
-8twokfivel9
-vfcsqvxkdxfiveqdvgqdmstn5
-5l63
-two8fourzskrqbcszfzbchlh9ldcp6
-hqhszsgmqzlksq5
-sb6fivefourpmtptjtkzhbxjjnqsixkt9
-twohrktppz5sevenhppmnjzlrkdqddsgs
-two37ninefive
-fourllczb9
-sixfourone83two
-ktgpc7
-fjsnkdj6sixsixtworlhgnbqlbm
-51zscxpk6onesevenjxxzcp6hqrtjmhqpk
-dmxfcfmfsbfpjfive4
-one47
-9jdlkcpzsevengfddvzxdnfkxf8
-fourdxnine3four39
-nine1one7fjcjjckngthreec
-5dlqjlbpt
-twooneeight9gf6zvtsqvrlnf
-three3six7
-3jnhfivethree
-1pzdqvjftwofive348
-four7kcrqkf9
-9cxglsdg
-twobgmghbrqdngthreervxjbmp7xvrskhfcf
-cpvhhkgmftttdtwoqfncthree1tzlbqcr5
-kmxqkfmlgtmztzpr74ninebqgcjkksljrphc
-mrsmtdhpsixslxg9five7
-53two
-xpfzv3
-twosdjhone551twozgqc4
-89fourfournfhc
-five7chqddxtwo1tjmlhqsix
-dkrnxgh5xqzcnjzrhg
-lcvfqpglmntwo1sixthreevdndckjgpkzpsp
-foursixnineseven1llbdvckff
-6four15fivettfivefive
-684cfnqfxkxgeightnfgqqmthreelbfxxdsmn
-fourdcxxseven28hxqqfhxtd
-1threegjffmjrfxppnsqthree
-3khnfmcmtj33
-9ninejvdl88
-3four9seven8fourmpjpkn7
-tmfourkc1sixfournglfl
-24xgscdtfxhttglvhczrstpfcjvnine2fiveone
-psqoneight4twojxkcvgdteight1rhcgmkmmjbbnzdhqj
-sfrgqk1two
-fiverzjbzssone4nineninefive
-twonineonergqsg2eight7eightwolf
-rztthree6sixsixxsxtvjthree
-78fourcvthree
-17hjphkdthree
-tdprffbgqseven7
-58eightbchzffmkhh8twofivethree
-zpbfstbb71hgldfkrvfourthreeonesixfour
-fiveseven1eightnine
-four8nine4vxpfpgxtlfhcrndscfgn4seven
-pgtznpnqvm1one1dfsix16
-ddffoureightpmqkznnseven75two
-6lklqx1sevenzhfdb1
-mq113scstpnnveightfive3nine
-threetwox79
-284mrsixthreefour
-1seven7zk4lldz2
-271nine2fourfive9
-fourthree37xxkvlgsixzpkblnine
-xbbnj2eight33
-seven5sevenonekzpnhzx
-247xgmlnntrcsixbstnine
-3ninezxtbqbfgtdjpgmjv
-tvxkssrfthree3
-fourfoureight12
-onefdszsvrzt2fdeightzkbmz
-cqrqkfgb3sevenqtqntxxhqlvrcthreefour
-2one5ptslgxsp4six4two6
-rskmbsfglone913vlmqtmpvfsevenp
-7c
-nkzrdb66crhk
-onevdttzljsmzvvhlf1tzqsqnnchdxbmngtlzzjdszvlvfzhx
-eightbtstrjzmfmzvcgsbgfxfour4one1
-pttthttfftkp41
-two9rlqrxvsevenfive
-v2four4
-two2one
-rdvhthhzrmeight5jtgf
-flshgbbtztkjfive8
-7sfc181fivefive
-fivenine1bfnchprbsix
-six2zpqshtndsgsevenone3one4
-fq8
-seven4eightvzfq7kthqh
-4vxtllmlnine8gsqkngfdzeight
-vhfzmbgseven5
-skqfzlconefivertzchfkvthreeeightfive22
-72oneeightone
-7ccs8vjx7vvszsn
-xrtmgqk95five849
-threebqeight8hg
-drdhjjtdrdxonenineninefourfkzrrggvz97
-8xxldtmdctllqssgdqp83
-dfqrjzv9rqbtn6
-3ninenhgqkglfvjbmgcdrsbhfournine
-five821
-54foursix7pv2qsix
-7197threescjkqhpqvzgjthpmcgtzrcd
-ltpzstwo78fivefourstwox
-mcqcmxxzcmpzrz4ntgnsgqbqjmkzpqvxtvsixrzzr3seven
-foursixfourzrnxsixgpx7eight
-41448sevenhxjpbvhvlmqrpjsvhblts
-1geightgtxlzdmpprjvg856five
-2tgrll648four
-3pkcd6eight948
-94sfznqjqlkvfjgczm
-twockgseven4seven6bp
-sixsix6eightsixeight
-nine3threenpsmshnchm
-threemqfptponesevendbjs17
-2ninehnsnnvj21fkeightwodmz
-jcptspngbc38nvtnrmvqtwo1
-6qsmcvfoursmlsevensix4lkpxxcnk
-xmtjrsrkjd5
-7psvffqn4
-3sh
-jdklghtbz1eightrhvfmnlknlghg77
-62tbtjfkltkdrxsxhhxpvbfvpnrpflh
-fpctmmvvnbftv2
-nkxmdshm5twoseven672
-88788jnscmpqr66sxcjx
diff --git a/aoc2023/day2/eg.txt b/aoc2023/day2/eg.txt
deleted file mode 100644
index 295c36d..0000000
--- a/aoc2023/day2/eg.txt
+++ /dev/null
@@ -1,5 +0,0 @@
-Game 1: 3 blue, 4 red; 1 red, 2 green, 6 blue; 2 green
-Game 2: 1 blue, 2 green; 3 green, 4 blue, 1 red; 1 green, 1 blue
-Game 3: 8 green, 6 blue, 20 red; 5 blue, 4 red, 13 green; 5 green, 1 red
-Game 4: 1 green, 3 red, 6 blue; 3 green, 6 red; 3 green, 15 blue, 14 red
-Game 5: 6 red, 1 blue, 3 green; 2 blue, 1 red, 2 green
diff --git a/aoc2023/day3/eg.txt b/aoc2023/day3/eg.txt
deleted file mode 100644
index b20187f..0000000
--- a/aoc2023/day3/eg.txt
+++ /dev/null
@@ -1,10 +0,0 @@
-467..114..
-...*......
-..35..633.
-......#...
-617*......
-.....+.58.
-..592.....
-......755.
-...$.*....
-.664.598..
diff --git a/aoc2023/day4/eg.txt b/aoc2023/day4/eg.txt
deleted file mode 100644
index 9bdb874..0000000
--- a/aoc2023/day4/eg.txt
+++ /dev/null
@@ -1,6 +0,0 @@
-Card 1: 41 48 83 86 17 | 83 86  6 31 17  9 48 53
-Card 2: 13 32 20 16 61 | 61 30 68 82 17 32 24 19
-Card 3:  1 21 53 59 44 | 69 82 63 72 16 21 14  1
-Card 4: 41 92 73 84 69 | 59 84 76 51 58  5 54 83
-Card 5: 87 83 26 28 32 | 88 30 70 12 93 22 82 36
-Card 6: 31 18 13 56 72 | 74 77 10 23 35 67 36 11
diff --git a/aoc2023/day5/eg.txt b/aoc2023/day5/eg.txt
deleted file mode 100644
index f756727..0000000
--- a/aoc2023/day5/eg.txt
+++ /dev/null
@@ -1,33 +0,0 @@
-seeds: 79 14 55 13
-
-seed-to-soil map:
-50 98 2
-52 50 48
-
-soil-to-fertilizer map:
-0 15 37
-37 52 2
-39 0 15
-
-fertilizer-to-water map:
-49 53 8
-0 11 42
-42 0 7
-57 7 4
-
-water-to-light map:
-88 18 7
-18 25 70
-
-light-to-temperature map:
-45 77 23
-81 45 19
-68 64 13
-
-temperature-to-humidity map:
-0 69 1
-1 0 69
-
-humidity-to-location map:
-60 56 37
-56 93 4
diff --git a/aoc2023/day6/eg.txt b/aoc2023/day6/eg.txt
deleted file mode 100644
index 28f5ae9..0000000
--- a/aoc2023/day6/eg.txt
+++ /dev/null
@@ -1,2 +0,0 @@
-Time:      7  15   30
-Distance:  9  40  200
diff --git a/aoc2023/Aoc.newt b/aoc2024/Aoc.newt
similarity index 100%
rename from aoc2023/Aoc.newt
rename to aoc2024/Aoc.newt
diff --git a/aoc2024/Node.newt b/aoc2024/Node.newt
deleted file mode 120000
index 66718c9..0000000
--- a/aoc2024/Node.newt
+++ /dev/null
@@ -1 +0,0 @@
-../aoc2023/Node.newt
\ No newline at end of file
diff --git a/aoc2024/Node.newt b/aoc2024/Node.newt
new file mode 100644
index 0000000..98bcdb8
--- /dev/null
+++ b/aoc2024/Node.newt
@@ -0,0 +1,7 @@
+module Node
+
+import Prelude
+
+pfunc fs : JSObject := `require('fs')`
+pfunc getArgs : List String := `arrayToList(String, process.argv)`
+pfunc readFile uses (MkIORes) : (fn : String) -> IO String := `(fn) => (w) => Prelude_MkIORes(require('fs').readFileSync(fn, 'utf8'), w)`
diff --git a/aoc2024/SortedMap.newt b/aoc2024/SortedMap.newt
deleted file mode 120000
index ef4aa42..0000000
--- a/aoc2024/SortedMap.newt
+++ /dev/null
@@ -1 +0,0 @@
-../newt/SortedMap.newt
\ No newline at end of file
diff --git a/aoc2024/SortedMap.newt b/aoc2024/SortedMap.newt
new file mode 100644
index 0000000..9a65b1b
--- /dev/null
+++ b/aoc2024/SortedMap.newt
@@ -0,0 +1,203 @@
+module SortedMap
+
+import Prelude
+
+-- TODO We'll want to replace Ord/Eq with (a → Ordering) (and rewrite most of our aoc solutions...)
+-- data Ordering : U where
+--   LT EQ GT : Ordering
+
+data T23 : Nat -> U -> U -> U where
+  Leaf : ∀ k v. k -> v -> T23 Z k v
+  Node2 : ∀ h k v. T23 h k v -> k -> T23 h k v -> T23 (S h) k v
+  Node3 : ∀ h k v. T23 h k v -> k -> T23 h k v -> k -> T23 h k v -> T23 (S h) k v
+
+lookupT23 : ∀ h k v. {{Ord k}} {{Eq k}} -> k -> T23 h k v -> Maybe (k × v)
+lookupT23 key (Leaf k v)= if k == key then Just (k,v) else Nothing
+lookupT23 key (Node2 t1 k1 t2) =
+  if key <= k1 then lookupT23 key t1 else lookupT23 key t2
+lookupT23 key (Node3 t1 k1 t2 k2 t3) =
+  if key <= k1 then lookupT23 key t1
+  else if key <= k2 then lookupT23 key t2
+  else lookupT23 key t3
+
+insertT23 : ∀ h k v. {{Ord k}} {{Eq k}} -> k -> v -> T23 h k v -> Either (T23 h k v) (T23 h k v × k × T23 h k v)
+insertT23 key value (Leaf k v) =
+  if key == k then Left (Leaf key value)
+  else if key <= k then Right (Leaf key value, key, Leaf k v)
+  else Right (Leaf k v, k, Leaf key value)
+insertT23 key value (Node2 t1 k1 t2) =
+  if key <= k1 then
+    case insertT23 key value t1 of
+      Left t1' => Left (Node2 t1' k1 t2)
+      Right (a,b,c) => Left (Node3 a b c k1 t2)
+  else case insertT23 key value t2 of
+      Left t2' => Left (Node2 t1 k1 t2')
+      Right (a,b,c) => Left (Node3 t1 k1 a b c)
+insertT23 key value (Node3 t1 k1 t2 k2 t3) =
+  if key <= k1 then
+    case insertT23 key value t1 of
+      Left t1' => Left (Node3 t1' k1 t2 k2 t3)
+      Right (a,b,c) => Right (Node2 a b c, k1, Node2 t2 k2 t3)
+  else if key <= k2 then
+    case insertT23 key value t2 of
+      Left t2' => Left (Node3 t1 k1 t2' k2 t3)
+      Right (a,b,c) => Right (Node2 t1 k1 a, b, Node2 c k2 t3)
+  else
+    case insertT23 key value t3 of
+      Left t3' => Left (Node3 t1 k1 t2 k2 t3')
+      Right (a,b,c) => Right (Node2 t1 k1 t2, k2, Node2 a b c)
+
+-- This is cribbed from Idris. Deleting nodes takes a bit of code.
+Hole : Nat → U → U → U
+Hole Z k v = Unit
+Hole (S n) k v = T23 n k v
+
+Node4 : ∀ k v h. T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → T23 (S (S h)) k v
+Node4 t1 k1 t2 k2 t3 k3 t4 = Node2 (Node2 t1 k1 t2) k2 (Node2 t3 k3 t4)
+
+Node5 : ∀ k v h. T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → T23 (S (S h)) k v
+Node5 a b c d e f g h i = Node2 (Node2 a b c) d (Node3 e f g h i)
+
+Node6 : ∀ k v h. T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → T23 (S (S h)) k v
+Node6 a b c d e f g h i j k = Node2 (Node3 a b c d e) f (Node3 g h i j k)
+
+Node7 : ∀ k v h. T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → T23 (S (S h)) k v
+Node7 a b c d e f g h i j k l m = Node3 (Node3 a b c d e) f (Node2 g h i) j (Node2 k l m)
+
+merge1 : ∀ k v h. T23 h k v → k → T23 (S h) k v → k → T23 (S h) k v → T23 (S (S h)) k v
+merge1 a b (Node2 c d e) f (Node2 g h i) = Node5 a b c d e f g h i
+merge1 a b (Node2 c d e) f (Node3 g h i j k) = Node6 a b c d e f g h i j k
+merge1 a b (Node3 c d e f g) h (Node2 i j k) = Node6 a b c d e f g h i j k
+merge1 a b (Node3 c d e f g) h (Node3 i j k l m) = Node7 a b c d e f g h i j k l m
+
+merge2 : ∀ k v h. T23 (S h) k v → k → T23 h k v → k → T23 (S h) k v → T23 (S (S h)) k v
+merge2 (Node2 a b c) d e f (Node2 g h i) = Node5 a b c d e f g h i
+merge2 (Node2 a b c) d e f (Node3 g h i j k) = Node6 a b c d e f g h i j k
+merge2 (Node3 a b c d e) f g h (Node2 i j k) = Node6 a b c d e f g h i j k
+merge2 (Node3 a b c d e) f g h (Node3 i j k l m) = Node7 a b c d e f g h i j k l m
+
+merge3 : ∀ k v h. T23 (S h) k v → k → T23 (S h) k v → k → T23 h k v → T23 (S (S h)) k v
+merge3 (Node2 a b c) d (Node2 e f g) h i = Node5 a b c d e f g h i
+merge3 (Node2 a b c) d (Node3 e f g h i) j k = Node6 a b c d e f g h i j k
+merge3 (Node3 a b c d e) f (Node2 g h i) j k = Node6 a b c d e f g h i j k
+merge3 (Node3 a b c d e) f (Node3 g h i j k) l m = Node7 a b c d e f g h i j k l m
+
+-- height is erased in the data everywhere but the top, but needed for case
+-- I wonder if we could use a 1 + 1 + 1 type instead of Either Tree Hole and condense this
+deleteT23 : ∀ k v. {{Ord k}} {{Eq k}} → (h : Nat) -> k -> T23 h k v -> Either (T23 h k v) (Hole h k v)
+deleteT23 Z key (Leaf k v) = if k == key then Right MkUnit else Left (Leaf k v)
+deleteT23 (S Z) key (Node2 t1 k1 t2) =
+  if key <= k1
+  then case deleteT23 Z key t1 of
+    Left t1 => Left (Node2 t1 k1 t2)
+    Right _ => Right t2
+  else case deleteT23 Z key t2 of
+    Left t2 => Left (Node2 t1 k1 t2)
+    Right MkUnit => Right t1
+deleteT23 (S Z) key (Node3 t1 k1 t2 k2 t3) =
+  if key <= k1
+  then case deleteT23 _ key t1 of
+    Left t1 => Left (Node3 t1 k1 t2 k2 t3)
+    Right MkUnit => Left (Node2 t2 k2 t3)
+  else if key <= k2 then case deleteT23 _ key t2 of
+    Left t2 => Left (Node3 t1 k1 t2 k2 t3)
+    Right _ => Left (Node2 t1 k1 t3)
+  else case deleteT23 _ key t3 of
+    Left t3 => Left (Node3 t1 k1 t2 k2 t3)
+    Right _ => Left (Node2 t1 k1 t2)
+deleteT23 (S (S h)) key (Node2 t1 k1 t2) =
+  if key <= k1
+  then case deleteT23 (S h) key t1 of
+    Left t1 => Left (Node2 t1 k1 t2)
+    Right t1 => case t2 of
+      Node2 t2' k2' t3' => Right (Node3 t1 k1 t2' k2' t3')
+      Node3 t2 k2 t3 k3 t4 => Left $ Node4 t1 k1 t2 k2 t3 k3 t4
+  else case deleteT23 _ key t2 of
+    Left t2 => Left (Node2 t1 k1 t2)
+    Right t2 => case t1 of
+      Node2 a b c => Right (Node3 a b c k1 t2)
+      Node3 a b c d e => Left (Node4 a b c d e k1 t2)
+deleteT23 (S (S h)) key (Node3 t1 k1 t2 k2 t3) =
+  if key <= k1
+  then case deleteT23 _ key t1 of
+    Left t1 => Left (Node3 t1 k1 t2 k2 t3)
+    Right t1 => Left (merge1 t1 k1 t2 k2 t3)
+  else if key <= k2 then case deleteT23 _ key t2 of
+    Left t2 => Left (Node3 t1 k1 t2 k2 t3)
+    Right t2 => Left (merge2 t1 k1 t2 k2 t3)
+  else case deleteT23 _ key t3 of
+    Left t3 => Left (Node3 t1 k1 t2 k2 t3)
+    Right t3 => Left (merge3 t1 k1 t2 k2 t3)
+
+treeLeft : ∀ h k v. T23 h k v → (k × v)
+treeLeft (Leaf k v) = (k, v)
+treeLeft (Node2 t1 _ _) = treeLeft t1
+treeLeft (Node3 t1 _ _ _ _) = treeLeft t1
+
+treeRight : ∀ h k v. T23 h k v → (k × v)
+treeRight (Leaf k v) = (k, v)
+treeRight (Node2 _ _ t2) = treeRight t2
+treeRight (Node3 _ _ _ _ t3) = treeRight t3
+
+
+data SortedMap : U -> U -> U where
+  EmptyMap : ∀ k v. SortedMap k v
+  -- not erased so we know what happens in delete
+  MapOf : ∀ k v. {h : Nat} →  T23 h k v -> SortedMap k v
+
+deleteMap : ∀ k v. {{Ord k}} {{Eq k}} → k → SortedMap k v → SortedMap k v
+deleteMap key EmptyMap = EmptyMap
+-- REVIEW if I split h separately in a nested case, it doesn't sort out Hole
+deleteMap key (MapOf {k} {v} {Z} tree) = case deleteT23 Z key tree of
+  Left t => MapOf t
+  Right t => EmptyMap
+deleteMap key (MapOf {k} {v} {S n} tree) = case deleteT23 (S n) key tree of
+  Left t => MapOf t
+  Right t => MapOf t
+
+leftMost : ∀ k v. SortedMap k v → Maybe (k × v)
+leftMost EmptyMap = Nothing
+leftMost (MapOf m) = Just (treeLeft m)
+
+rightMost : ∀ k v. SortedMap k v → Maybe (k × v)
+rightMost EmptyMap = Nothing
+rightMost (MapOf m) = Just (treeRight m)
+
+-- TODO issue with metas and case if written as `do` block
+pop : ∀ k v. {{Eq k}} {{Ord k}} → SortedMap k v → Maybe ((k × v) × SortedMap k v)
+pop m = case leftMost m of
+    Just (k,v) => Just ((k,v), deleteMap k m)
+    Nothing => Nothing
+
+lookupMap : ∀ k v. {{Ord k}} {{Eq k}} -> k -> SortedMap k v -> Maybe (k × v)
+lookupMap k EmptyMap = Nothing
+lookupMap k (MapOf map) = lookupT23 k map
+
+lookupMap' : ∀ k v. {{Ord k}} {{Eq k}} -> k -> SortedMap k v -> Maybe v
+lookupMap' k EmptyMap = Nothing
+lookupMap' k (MapOf map) = snd <$> lookupT23 k map
+
+
+updateMap : ∀ k v. {{Ord k}} {{Eq k}} -> k -> v -> SortedMap k v -> SortedMap k v
+updateMap k v EmptyMap = MapOf $ Leaf k v
+updateMap k v (MapOf map) = case insertT23 k v map of
+  Left map' => MapOf map'
+  Right (a, b, c) => MapOf (Node2 a b c)
+
+toList : ∀ k v. SortedMap k v → List (k × v)
+toList {k} {v} (MapOf smap) = reverse $ go smap Nil
+  where
+    go : ∀ h. T23 h k v → List (k × v) → List (k × v)
+    go (Leaf k v) acc = (k, v) :: acc
+    go (Node2 t1 k1 t2) acc = go t2 (go t1 acc)
+    go (Node3 t1 k1 t2 k2 t3) acc = go t3 $ go t2 $ go t1 acc
+toList _ = Nil
+
+foldMap : ∀ a b. {{Ord a}} {{Eq a}} → (b → b → b) → SortedMap a b → List (a × b) → SortedMap a b
+foldMap f m Nil = m
+foldMap f m ((a,b) :: xs) = case lookupMap a m of
+  Nothing => foldMap f (updateMap a b m) xs
+  Just (_, b') => foldMap f (updateMap a (f b' b) m) xs
+
+listValues : ∀ k v. SortedMap k v → List v
+listValues sm = map snd $ toList sm
diff --git a/newt/SortedMap.newt b/newt/SortedMap.newt
deleted file mode 100644
index 9a65b1b..0000000
--- a/newt/SortedMap.newt
+++ /dev/null
@@ -1,203 +0,0 @@
-module SortedMap
-
-import Prelude
-
--- TODO We'll want to replace Ord/Eq with (a → Ordering) (and rewrite most of our aoc solutions...)
--- data Ordering : U where
---   LT EQ GT : Ordering
-
-data T23 : Nat -> U -> U -> U where
-  Leaf : ∀ k v. k -> v -> T23 Z k v
-  Node2 : ∀ h k v. T23 h k v -> k -> T23 h k v -> T23 (S h) k v
-  Node3 : ∀ h k v. T23 h k v -> k -> T23 h k v -> k -> T23 h k v -> T23 (S h) k v
-
-lookupT23 : ∀ h k v. {{Ord k}} {{Eq k}} -> k -> T23 h k v -> Maybe (k × v)
-lookupT23 key (Leaf k v)= if k == key then Just (k,v) else Nothing
-lookupT23 key (Node2 t1 k1 t2) =
-  if key <= k1 then lookupT23 key t1 else lookupT23 key t2
-lookupT23 key (Node3 t1 k1 t2 k2 t3) =
-  if key <= k1 then lookupT23 key t1
-  else if key <= k2 then lookupT23 key t2
-  else lookupT23 key t3
-
-insertT23 : ∀ h k v. {{Ord k}} {{Eq k}} -> k -> v -> T23 h k v -> Either (T23 h k v) (T23 h k v × k × T23 h k v)
-insertT23 key value (Leaf k v) =
-  if key == k then Left (Leaf key value)
-  else if key <= k then Right (Leaf key value, key, Leaf k v)
-  else Right (Leaf k v, k, Leaf key value)
-insertT23 key value (Node2 t1 k1 t2) =
-  if key <= k1 then
-    case insertT23 key value t1 of
-      Left t1' => Left (Node2 t1' k1 t2)
-      Right (a,b,c) => Left (Node3 a b c k1 t2)
-  else case insertT23 key value t2 of
-      Left t2' => Left (Node2 t1 k1 t2')
-      Right (a,b,c) => Left (Node3 t1 k1 a b c)
-insertT23 key value (Node3 t1 k1 t2 k2 t3) =
-  if key <= k1 then
-    case insertT23 key value t1 of
-      Left t1' => Left (Node3 t1' k1 t2 k2 t3)
-      Right (a,b,c) => Right (Node2 a b c, k1, Node2 t2 k2 t3)
-  else if key <= k2 then
-    case insertT23 key value t2 of
-      Left t2' => Left (Node3 t1 k1 t2' k2 t3)
-      Right (a,b,c) => Right (Node2 t1 k1 a, b, Node2 c k2 t3)
-  else
-    case insertT23 key value t3 of
-      Left t3' => Left (Node3 t1 k1 t2 k2 t3')
-      Right (a,b,c) => Right (Node2 t1 k1 t2, k2, Node2 a b c)
-
--- This is cribbed from Idris. Deleting nodes takes a bit of code.
-Hole : Nat → U → U → U
-Hole Z k v = Unit
-Hole (S n) k v = T23 n k v
-
-Node4 : ∀ k v h. T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → T23 (S (S h)) k v
-Node4 t1 k1 t2 k2 t3 k3 t4 = Node2 (Node2 t1 k1 t2) k2 (Node2 t3 k3 t4)
-
-Node5 : ∀ k v h. T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → T23 (S (S h)) k v
-Node5 a b c d e f g h i = Node2 (Node2 a b c) d (Node3 e f g h i)
-
-Node6 : ∀ k v h. T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → T23 (S (S h)) k v
-Node6 a b c d e f g h i j k = Node2 (Node3 a b c d e) f (Node3 g h i j k)
-
-Node7 : ∀ k v h. T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → T23 (S (S h)) k v
-Node7 a b c d e f g h i j k l m = Node3 (Node3 a b c d e) f (Node2 g h i) j (Node2 k l m)
-
-merge1 : ∀ k v h. T23 h k v → k → T23 (S h) k v → k → T23 (S h) k v → T23 (S (S h)) k v
-merge1 a b (Node2 c d e) f (Node2 g h i) = Node5 a b c d e f g h i
-merge1 a b (Node2 c d e) f (Node3 g h i j k) = Node6 a b c d e f g h i j k
-merge1 a b (Node3 c d e f g) h (Node2 i j k) = Node6 a b c d e f g h i j k
-merge1 a b (Node3 c d e f g) h (Node3 i j k l m) = Node7 a b c d e f g h i j k l m
-
-merge2 : ∀ k v h. T23 (S h) k v → k → T23 h k v → k → T23 (S h) k v → T23 (S (S h)) k v
-merge2 (Node2 a b c) d e f (Node2 g h i) = Node5 a b c d e f g h i
-merge2 (Node2 a b c) d e f (Node3 g h i j k) = Node6 a b c d e f g h i j k
-merge2 (Node3 a b c d e) f g h (Node2 i j k) = Node6 a b c d e f g h i j k
-merge2 (Node3 a b c d e) f g h (Node3 i j k l m) = Node7 a b c d e f g h i j k l m
-
-merge3 : ∀ k v h. T23 (S h) k v → k → T23 (S h) k v → k → T23 h k v → T23 (S (S h)) k v
-merge3 (Node2 a b c) d (Node2 e f g) h i = Node5 a b c d e f g h i
-merge3 (Node2 a b c) d (Node3 e f g h i) j k = Node6 a b c d e f g h i j k
-merge3 (Node3 a b c d e) f (Node2 g h i) j k = Node6 a b c d e f g h i j k
-merge3 (Node3 a b c d e) f (Node3 g h i j k) l m = Node7 a b c d e f g h i j k l m
-
--- height is erased in the data everywhere but the top, but needed for case
--- I wonder if we could use a 1 + 1 + 1 type instead of Either Tree Hole and condense this
-deleteT23 : ∀ k v. {{Ord k}} {{Eq k}} → (h : Nat) -> k -> T23 h k v -> Either (T23 h k v) (Hole h k v)
-deleteT23 Z key (Leaf k v) = if k == key then Right MkUnit else Left (Leaf k v)
-deleteT23 (S Z) key (Node2 t1 k1 t2) =
-  if key <= k1
-  then case deleteT23 Z key t1 of
-    Left t1 => Left (Node2 t1 k1 t2)
-    Right _ => Right t2
-  else case deleteT23 Z key t2 of
-    Left t2 => Left (Node2 t1 k1 t2)
-    Right MkUnit => Right t1
-deleteT23 (S Z) key (Node3 t1 k1 t2 k2 t3) =
-  if key <= k1
-  then case deleteT23 _ key t1 of
-    Left t1 => Left (Node3 t1 k1 t2 k2 t3)
-    Right MkUnit => Left (Node2 t2 k2 t3)
-  else if key <= k2 then case deleteT23 _ key t2 of
-    Left t2 => Left (Node3 t1 k1 t2 k2 t3)
-    Right _ => Left (Node2 t1 k1 t3)
-  else case deleteT23 _ key t3 of
-    Left t3 => Left (Node3 t1 k1 t2 k2 t3)
-    Right _ => Left (Node2 t1 k1 t2)
-deleteT23 (S (S h)) key (Node2 t1 k1 t2) =
-  if key <= k1
-  then case deleteT23 (S h) key t1 of
-    Left t1 => Left (Node2 t1 k1 t2)
-    Right t1 => case t2 of
-      Node2 t2' k2' t3' => Right (Node3 t1 k1 t2' k2' t3')
-      Node3 t2 k2 t3 k3 t4 => Left $ Node4 t1 k1 t2 k2 t3 k3 t4
-  else case deleteT23 _ key t2 of
-    Left t2 => Left (Node2 t1 k1 t2)
-    Right t2 => case t1 of
-      Node2 a b c => Right (Node3 a b c k1 t2)
-      Node3 a b c d e => Left (Node4 a b c d e k1 t2)
-deleteT23 (S (S h)) key (Node3 t1 k1 t2 k2 t3) =
-  if key <= k1
-  then case deleteT23 _ key t1 of
-    Left t1 => Left (Node3 t1 k1 t2 k2 t3)
-    Right t1 => Left (merge1 t1 k1 t2 k2 t3)
-  else if key <= k2 then case deleteT23 _ key t2 of
-    Left t2 => Left (Node3 t1 k1 t2 k2 t3)
-    Right t2 => Left (merge2 t1 k1 t2 k2 t3)
-  else case deleteT23 _ key t3 of
-    Left t3 => Left (Node3 t1 k1 t2 k2 t3)
-    Right t3 => Left (merge3 t1 k1 t2 k2 t3)
-
-treeLeft : ∀ h k v. T23 h k v → (k × v)
-treeLeft (Leaf k v) = (k, v)
-treeLeft (Node2 t1 _ _) = treeLeft t1
-treeLeft (Node3 t1 _ _ _ _) = treeLeft t1
-
-treeRight : ∀ h k v. T23 h k v → (k × v)
-treeRight (Leaf k v) = (k, v)
-treeRight (Node2 _ _ t2) = treeRight t2
-treeRight (Node3 _ _ _ _ t3) = treeRight t3
-
-
-data SortedMap : U -> U -> U where
-  EmptyMap : ∀ k v. SortedMap k v
-  -- not erased so we know what happens in delete
-  MapOf : ∀ k v. {h : Nat} →  T23 h k v -> SortedMap k v
-
-deleteMap : ∀ k v. {{Ord k}} {{Eq k}} → k → SortedMap k v → SortedMap k v
-deleteMap key EmptyMap = EmptyMap
--- REVIEW if I split h separately in a nested case, it doesn't sort out Hole
-deleteMap key (MapOf {k} {v} {Z} tree) = case deleteT23 Z key tree of
-  Left t => MapOf t
-  Right t => EmptyMap
-deleteMap key (MapOf {k} {v} {S n} tree) = case deleteT23 (S n) key tree of
-  Left t => MapOf t
-  Right t => MapOf t
-
-leftMost : ∀ k v. SortedMap k v → Maybe (k × v)
-leftMost EmptyMap = Nothing
-leftMost (MapOf m) = Just (treeLeft m)
-
-rightMost : ∀ k v. SortedMap k v → Maybe (k × v)
-rightMost EmptyMap = Nothing
-rightMost (MapOf m) = Just (treeRight m)
-
--- TODO issue with metas and case if written as `do` block
-pop : ∀ k v. {{Eq k}} {{Ord k}} → SortedMap k v → Maybe ((k × v) × SortedMap k v)
-pop m = case leftMost m of
-    Just (k,v) => Just ((k,v), deleteMap k m)
-    Nothing => Nothing
-
-lookupMap : ∀ k v. {{Ord k}} {{Eq k}} -> k -> SortedMap k v -> Maybe (k × v)
-lookupMap k EmptyMap = Nothing
-lookupMap k (MapOf map) = lookupT23 k map
-
-lookupMap' : ∀ k v. {{Ord k}} {{Eq k}} -> k -> SortedMap k v -> Maybe v
-lookupMap' k EmptyMap = Nothing
-lookupMap' k (MapOf map) = snd <$> lookupT23 k map
-
-
-updateMap : ∀ k v. {{Ord k}} {{Eq k}} -> k -> v -> SortedMap k v -> SortedMap k v
-updateMap k v EmptyMap = MapOf $ Leaf k v
-updateMap k v (MapOf map) = case insertT23 k v map of
-  Left map' => MapOf map'
-  Right (a, b, c) => MapOf (Node2 a b c)
-
-toList : ∀ k v. SortedMap k v → List (k × v)
-toList {k} {v} (MapOf smap) = reverse $ go smap Nil
-  where
-    go : ∀ h. T23 h k v → List (k × v) → List (k × v)
-    go (Leaf k v) acc = (k, v) :: acc
-    go (Node2 t1 k1 t2) acc = go t2 (go t1 acc)
-    go (Node3 t1 k1 t2 k2 t3) acc = go t3 $ go t2 $ go t1 acc
-toList _ = Nil
-
-foldMap : ∀ a b. {{Ord a}} {{Eq a}} → (b → b → b) → SortedMap a b → List (a × b) → SortedMap a b
-foldMap f m Nil = m
-foldMap f m ((a,b) :: xs) = case lookupMap a m of
-  Nothing => foldMap f (updateMap a b m) xs
-  Just (_, b') => foldMap f (updateMap a (f b' b) m) xs
-
-listValues : ∀ k v. SortedMap k v → List v
-listValues sm = map snd $ toList sm
diff --git a/pack.toml b/pack.toml
deleted file mode 100644
index 40e9f1a..0000000
--- a/pack.toml
+++ /dev/null
@@ -1,10 +0,0 @@
-[custom.all.newt]
-type = "local"
-path = "."
-ipkg = "newt.ipkg"
-test = "test/test.ipkg"
-
-[custom.all.newt-test]
-type = "local"
-path = "test"
-ipkg = "test.ipkg"
\ No newline at end of file
diff --git a/src/Lib/CompileExp.newt b/src/Lib/CompileExp.newt
index e1bf219..24e1b55 100644
--- a/src/Lib/CompileExp.newt
+++ b/src/Lib/CompileExp.newt
@@ -87,8 +87,6 @@ any : ∀ a. (a → Bool) → List a → Bool
 any f Nil = False
 any f (x :: xs) = if f x then True else any f xs
 
--- NOW so we stuff quant and the args in here and sort it out later?
-
 -- apply an expression at an arity to a list of args
 -- CAppRef will specify any missing args, for eta conversion later
 -- and any extra args get individual CApp.