toki/advent-of-code-2024
1
0
Fork 0
Code Issues Pull requests Activity

style: decrease indentation on TTImp quote

Browse source
This commit is contained in:
Kiana Sheibani 2024-12-05 06:06:16 -05:00
parent b37d5f2dd4
commit 07b830672b
Signed by: toki
GPG key ID: 6CB106C25E86A9F7
1 changed files with 13 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
src/Data/Problem.idr
View file

@ -82,22 +82,24 @@ public export
fetchSolution : Problem -> Elab (String -> String) fetchSolution : Problem -> Elab (String -> String)
fetchSolution pr = do fetchSolution pr = do
let name = solutionName pr let name = solutionName pr
check `(\s => show (~(IVar EmptyFC name) s)) check `(\s => Prelude.show (~(IVar EmptyFC name) s))
<|> fail "\{show name} does not exist as a valid solution" <|> fail "\{show name} does not exist as a valid solution"
public export public export
fetchAllSols : (latest : Problem) -> Elab (SortedMap Problem (String -> String)) fetchAllSols : (latest : Problem) -> Elab (SortedMap Problem (String -> String))
fetchAllSols pr = fetchAllSols pr =
let prs = allProblems pr let prs = allProblems pr
list = foldr (\pr,tt => `(Prelude.(::) list = foldr
(Builtin.MkPair (\pr,tt =>
(Data.Problem.Pr `(Prelude.(::)
(Prelude.fromInteger (Builtin.MkPair
~(IPrimVal EmptyFC $ BI $ natToInteger pr.day)) (Data.Problem.Pr
~(case pr.part of (Prelude.fromInteger
Part1 => `(Data.Problem.Part1) ~(IPrimVal EmptyFC $ BI $ natToInteger pr.day))
Part2 => `(Data.Problem.Part2))) ~(case pr.part of
(\s => show (~(IVar EmptyFC $ solutionName pr) s))) Part1 => `(Data.Problem.Part1)
~(tt))) `(Prelude.Nil) prs Part2 => `(Data.Problem.Part2)))
(\s => Prelude.show (~(IVar EmptyFC $ solutionName pr) s)))
~(tt))) `(Prelude.Nil) prs
ttimp = `(Data.SortedMap.fromList ~(list)) ttimp = `(Data.SortedMap.fromList ~(list))
in check ttimp in check ttimp