diff --git a/aoc2024/Day17.newt b/aoc2024/Day17.newt index 15a7b82..7d80f61 100644 --- a/aoc2024/Day17.newt +++ b/aoc2024/Day17.newt @@ -80,10 +80,6 @@ step mach@(M a b c mem ip out) = combo 6 = c combo n = itobi n -find : ∀ a. (a → Bool) → List a → Maybe a -find f Nil = Nothing -find f (x :: xs) = if f x then Just x else find f xs - Cand : U Cand = BigInt × SnocList Int × List Int diff --git a/src/Lib/ProcessDecl.idr b/src/Lib/ProcessDecl.idr index b99cc05..a1b8a57 100644 --- a/src/Lib/ProcessDecl.idr +++ b/src/Lib/ProcessDecl.idr @@ -207,7 +207,7 @@ processDecl (TypeSig fc names tm) = do let mstart = length mc.metas for_ names $ \nm => do let Nothing := lookup nm top - | _ => error fc "\{show nm} is already defined" + | Just entry => error fc "\{show nm} is already defined at \{show entry.fc}" pure () ty <- check (mkCtx fc) tm (VU fc) ty <- zonk top 0 [] ty @@ -241,7 +241,7 @@ processDecl (Def fc nm clauses) = do let Just entry = lookup nm top | Nothing => throwError $ E fc "No declaration for \{nm}" let (MkEntry fc name ty Axiom) := entry - | _ => throwError $ E fc "\{nm} already defined" + | _ => throwError $ E fc "\{nm} already defined at \{show entry.fc}" putStrLn "check \{nm} at \{pprint [] ty}" vty <- eval empty CBN ty diff --git a/src/Lib/TopContext.idr b/src/Lib/TopContext.idr index fc2ca72..ecf1a97 100644 --- a/src/Lib/TopContext.idr +++ b/src/Lib/TopContext.idr @@ -45,8 +45,8 @@ setDef name fc ty def = do where go : List TopEntry -> M (List TopEntry) go [] = pure $ [MkEntry fc name ty def] - go (x@(MkEntry _ nm ty' def') :: defs) = if nm == name - then error fc "\{name} is already defined" + go (x@(MkEntry fc' nm ty' def') :: defs) = if nm == name + then error fc "\{name} is already defined at \{show fc'}" else (x ::) <$> go defs public export