diff --git a/TODO.md b/TODO.md
index 472d7f7..e997625 100644
--- a/TODO.md
+++ b/TODO.md
@@ -9,7 +9,7 @@ More comments in code! This is getting big enough that I need to re-find my bear
 - [x] for parse error, seek to col 0 token and process next decl
 - [ ] record update sugar, syntax TBD
   - I think I'm going to hold off on this for now as it requires the type to elaborate. This ends up at the head of an app, which typically is inferred. We'd need a special case somewhere that infers its argument instead.
-- [ ] Change `Ord` to be more like Idris - LT / EQ / GT (and entail equality)
+- [x] Change `Ord` to be more like Idris - LT / EQ / GT (and entail equality)
 - [ ] Keep a `compare` function on `SortedMap` (like lean)
 - [x] keymap for monaco
 - [x] SortedMap.newt issue in `where`
diff --git a/aoc2024/Day13.newt b/aoc2024/Day13.newt
index e0adae9..b7ddfee 100644
--- a/aoc2024/Day13.newt
+++ b/aoc2024/Day13.newt
@@ -51,7 +51,7 @@ instance Sub BigInt where a - b = subbi a b
 instance Cast Int BigInt where cast x = itobi x
 instance Eq BigInt where a == b = jsEq a b
 instance Show BigInt where show = jsShow
-instance Ord BigInt where a < b = jsLT a b
+instance Ord BigInt where compare a b = jsCompare a b
 
 calcCost : BigInt → Machine → Maybe BigInt
 calcCost extra (MkMachine (ax, ay) (bx, by) (px, py)) =
diff --git a/aoc2024/Day16.newt b/aoc2024/Day16.newt
index 7868368..56f61de 100644
--- a/aoc2024/Day16.newt
+++ b/aoc2024/Day16.newt
@@ -72,7 +72,7 @@ dirVal East = 2
 dirVal West = 3
 
 instance Ord Dir where
-  a < b = dirVal a < dirVal b
+  compare a b = compare (dirVal a) (dirVal b)
 
 instance Eq Dir where
   a == b = dirVal a == dirVal b
diff --git a/aoc2024/Day17.newt b/aoc2024/Day17.newt
index 7d80f61..c1c620f 100644
--- a/aoc2024/Day17.newt
+++ b/aoc2024/Day17.newt
@@ -21,7 +21,7 @@ instance Sub BigInt where a - b = subbi a b
 instance Cast Int BigInt where cast x = itobi x
 instance Eq BigInt where a == b = jsEq a b
 instance Show BigInt where show = jsShow
-instance Ord BigInt where a < b = jsLT a b
+instance Ord BigInt where compare a b = jsCompare a b
 
 data Machine : U where
   M : BigInt → BigInt → BigInt → List Int → Int → SnocList Int → Machine
diff --git a/aoc2024/Day22.newt b/aoc2024/Day22.newt
index c16885c..d653c68 100644
--- a/aoc2024/Day22.newt
+++ b/aoc2024/Day22.newt
@@ -23,7 +23,7 @@ instance Sub BigInt where a - b = subbi a b
 instance Cast Int BigInt where cast x = itobi x
 instance Eq BigInt where a == b = jsEq a b
 instance Show BigInt where show = jsShow
-instance Ord BigInt where a < b = jsLT a b
+instance Ord BigInt where compare a b = jsCompare a b
 
 infixl 7 _%_
 pfunc _%_ : BigInt → BigInt → BigInt := `(x,y) => x % y`
diff --git a/aoc2024/Day22b.newt b/aoc2024/Day22b.newt
index 78c4ac5..a11bc00 100644
--- a/aoc2024/Day22b.newt
+++ b/aoc2024/Day22b.newt
@@ -26,7 +26,7 @@ instance Sub BigInt where a - b = subbi a b
 instance Cast Int BigInt where cast x = itobi x
 instance Eq BigInt where a == b = jsEq a b
 instance Show BigInt where show = jsShow
-instance Ord BigInt where a < b = jsLT a b
+instance Ord BigInt where compare a b = jsCompare a b
 
 -- base: 30s
 -- switching from tuple to int: 8 s
diff --git a/aoc2024/Day24.newt b/aoc2024/Day24.newt
index a334135..292d805 100644
--- a/aoc2024/Day24.newt
+++ b/aoc2024/Day24.newt
@@ -18,7 +18,7 @@ instance Eq Op where
   _ == _ = False
 
 record Gate where
-  constructor GT
+  constructor MkG
   in1 : String
   in2 : String
   op : Op
@@ -49,7 +49,7 @@ parseFile text = do
     parseGate s = do
       let (in1 :: op :: in2 :: _ :: out :: Nil) = split s " " | _ => Left $ "bad gate: " ++ s
       op <- getOp op
-      Right $ GT in1 in2 op out
+      Right $ MkG in1 in2 op out
 
 
 State : U
@@ -114,10 +114,10 @@ range : Int → Int → List Int
 range a b = if a < b then a :: range (a + 1) b else Nil
 
 swapPins : String → String → Gate → Gate
-swapPins a g (GT i1 i2 op out) =
-  if out == a then GT i1 i2 op g
-  else if out == g then GT i1 i2 op a
-  else GT i1 i2 op out
+swapPins a g (MkG i1 i2 op out) =
+  if out == a then MkG i1 i2 op g
+  else if out == g then MkG i1 i2 op a
+  else MkG i1 i2 op out
 
 fail : ∀ a. String -> a
 fail msg = let x = trace "FAIL" msg in ?
diff --git a/aoc2024/Day6.newt b/aoc2024/Day6.newt
index 6be5533..c943cf4 100644
--- a/aoc2024/Day6.newt
+++ b/aoc2024/Day6.newt
@@ -28,7 +28,7 @@ instance Eq Dir where
   a == b = show a == show b
 
 instance Ord Dir where
-  a < b = show a < show b
+  compare a b = compare (show a) (show b)
 
 Done : U
 Done = SortedMap (Point × Dir) Unit
diff --git a/newt/Prelude.newt b/newt/Prelude.newt
index bc9b66f..97a4d9a 100644
--- a/newt/Prelude.newt
+++ b/newt/Prelude.newt
@@ -233,6 +233,7 @@ instance Concat String where
 
 pfunc jsEq uses (True False) : ∀ a. a → a → Bool := `(_, a, b) => a == b ? True : False`
 pfunc jsLT uses (True False) : ∀ a. a → a → Bool := `(_, a, b) => a < b ? True : False`
+
 pfunc jsShow : ∀ a . a → String := `(_,a) => ''+a`
 instance Eq Int where
   a == b = jsEq a b
@@ -662,39 +663,45 @@ tail : ∀ a. List a → List a
 tail Nil = Nil
 tail (x :: xs) = xs
 
---
+data Ordering = LT | EQ | GT
+instance Eq Ordering where
+  LT == LT = True
+  EQ == EQ = True
+  GT == GT = True
+  _ == _ = False
+
+-- FIXME There is a subtle issue here with shadowing if the file defines a GT in its own namespace
+-- We end up chosing that an assigning to GT, which cause a lot of trouble.
+-- Prelude.GT is not in scope, because we've depended on the other one.
+pfunc jsCompare uses (LT EQ GT) : ∀ a. a → a → Ordering := `(_, a, b) => a == b ? EQ : a < b ? LT : GT`
 
 infixl 6 _<_ _<=_ _>_
 class Ord a where
-  -- isEq : Eq a
-  _<_ : a → a → Bool
+  compare : a → a → Ordering
 
-_<=_ : ∀ a. {{Eq a}} {{Ord a}} → a → a → Bool
-a <= b = a == b || a < b
+_<_ : ∀ a. {{Ord a}} -> a → a → Bool
+a < b = compare a b == LT
+
+_<=_ : ∀ a. {{Ord a}} → a → a → Bool
+a <= b = compare a b /= GT
 
 _>_ : ∀ a. {{Ord a}} → a → a → Bool
-a > b = b < a
+a > b = compare a b == GT
 
 search : ∀ cl. {{cl}} -> cl
 search {{x}} = x
 
 instance Ord Nat where
-  -- isEq = search
-  _ < Z = False
-  Z < S _ = True
-  S n < S m = n < m
-
+  compare Z Z = EQ
+  compare _ Z = GT
+  compare Z (S _) = LT
+  compare (S n) (S m) = compare n m
 
 instance Ord Int where
-  -- isEq = ?
-  x < y = ltInt x y
+  compare a b = jsCompare a b
 
 instance Ord Char where
-  x < y = jsLT x y
-
--- foo : ∀ a. {{Ord a}} -> a -> Bool
--- foo a = a == a
-
+  compare a b = jsCompare a b
 
 flip : ∀ a b c. (a → b → c) → (b → a → c)
 flip f b a = f a b
@@ -724,7 +731,7 @@ ite : ∀ a. Bool → a → a → a
 ite c t e = if c then t else e
 
 instance Ord String where
-  a < b = jsLT a b
+  compare a b = jsCompare a b
 
 instance Cast Int Nat where
   cast n = intToNat n
@@ -738,8 +745,10 @@ swap (a,b) = (b,a)
 instance ∀ a b. {{Eq a}} {{Eq b}} → Eq (a × b) where
   (a,b) == (c,d) = a == c && b == d
 
-instance ∀ a b. {{Eq a}} {{Ord a}} {{Ord b}} → Ord (a × b) where
-  (a,b) < (c,d) = if a == c then b < d else a < c
+instance ∀ a b. {{Ord a}} {{Ord b}} → Ord (a × b) where
+  compare (a,b) (c,d) = case compare a c of
+    EQ => compare b d
+    res => res
 
 instance ∀ a. {{Eq a}} → Eq (List a) where
   Nil == Nil = True
diff --git a/src/Lib/Eval.idr b/src/Lib/Eval.idr
index 01efbe2..d9a1157 100644
--- a/src/Lib/Eval.idr
+++ b/src/Lib/Eval.idr
@@ -1,8 +1,5 @@
 module Lib.Eval
 
--- For FC
-import Lib.Parser.Impl
-import Lib.Prettier
 import Lib.Types
 import Lib.TopContext
 
@@ -13,10 +10,6 @@ import Data.SnocList
 import Data.Vect
 import Data.SortedMap
 
--- Need to wire in the metas...
--- if it's top / ctx / IORef, I also need IO...
--- if I want errors, I need m anyway.  I've already got an error down there.
-
 export
 eval : Env -> Mode -> Tm -> M Val
 
diff --git a/src/Lib/Parser.idr b/src/Lib/Parser.idr
index 4b413d2..86f25f8 100644
--- a/src/Lib/Parser.idr
+++ b/src/Lib/Parser.idr
@@ -1,19 +1,11 @@
 module Lib.Parser
-import Lib.Types
-import Debug.Trace
+
+import Data.Maybe
 import Data.String
-
--- app: foo {a} a b
--- lam: λ {A} {b : A} (c : Blah) d e f => something
--- lam: \ {A} {b : A} (c : Blah) d e f => something
--- pi: (A : Set) -> {b : A} -> (c : Foo b) -> c -> bar d
--- pi: (A B : Set) {b : A} -> (c : Foo b) -> c -> bar d
-
-import Lib.Token
 import Lib.Parser.Impl
 import Lib.Syntax
-import Data.List
-import Data.Maybe
+import Lib.Token
+import Lib.Types
 
 ident = token Ident <|> token MixFix
 
@@ -104,10 +96,6 @@ pArg = do
 
 AppSpine = List (Icit,FC,Raw)
 
--- helper for debugging
-traceM : Monad m => String -> m ()
-traceM msg = trace msg $ pure ()
-
 pratt : Operators -> Int -> String -> Raw -> AppSpine -> Parser (Raw, AppSpine)
 pratt ops prec stop left spine = do
   (left, spine) <- runPrefix stop left spine