diff --git a/db/posts/5.json b/db/posts/5.json
index 62306f6..d2043ff 100644
--- a/db/posts/5.json
+++ b/db/posts/5.json
@@ -1,5 +1,6 @@
 {
   "edited-at": [
+    "2025-02-14T12:00:50.492225-05:00"
   ],
   "hidden": false,
   "idris": true,
diff --git a/projects/Idris/src/LessMacrosMoreTypes/Printf.md b/projects/Idris/src/LessMacrosMoreTypes/Printf.md
index a6dcd5b..bddd1d3 100644
--- a/projects/Idris/src/LessMacrosMoreTypes/Printf.md
+++ b/projects/Idris/src/LessMacrosMoreTypes/Printf.md
@@ -11,7 +11,7 @@ While C can provide "convenient" string formatting by having hideously unsafe va
 
 This article is inspired by an exercise from chapter 6 of [Type Driven Development with Idris](https://www.manning.com/books/type-driven-development-with-idris), and is written as a literate Idris file, with the source available [here](https://git.stranger.systems/thatonelutenist/website/src/branch/trunk/projects/Idris/src/LessMacrosMoreTypes/Printf.md).
 
-## Gameplan
+## Game plan
 
 Our goal is to provide a `printf` function that can be called much like it's C equivalent:
 
@@ -29,7 +29,7 @@ Idris lacks a dedicated facility for variadics, but we can call functions in typ
 Idris allows us to manipulate types as first class values, and we can use the runtime values of previous arguments to the function we are declaring as arguments to later type-level functions. These type-level functions can, furthermore, recurse into themselves to produce type signatures of varying length and content.
 
 > [!TIP]
-> Idris requires that these type level functions be [_total_](https://idris2.readthedocs.io/en/latest/tutorial/theorems.html#totality-checking) for them to be expanded at compile time, meaning they are known to the compiler to return a value in constant time for all possible inputs.
+> Idris requires that these type level functions be [_total_](https://idris2.readthedocs.io/en/latest/tutorial/theorems.html#totality-checking) for them to be expanded at compile time, meaning they are known to the compiler to return a value in finite time for all possible inputs.
 
 This allows us to produce variadic functions, so long as the number of arguments and their types can be determined from one of the arguments of the function before the variadic portion.
 
@@ -43,7 +43,7 @@ First, we need a data structure to describe our format string. We define the `Fo
 data Format : Type where
   ||| A slot that should be filled in with a number
   Number : (next : Format) -> Format
-  ||| A slot that should be filled  in with a number, padded to a certian number
+  ||| A slot that should be filled  in with a number, padded to a certain number
   ||| of digits
   PaddedNumber : (digits : Nat) -> (next : Format) -> Format
   ||| A slot that should be filled in with a string
@@ -188,7 +188,7 @@ printfFmt (Just x) acc = printfFmt' x acc
 
 ### With a Format String
 
-`printf` is easily defined a simple wrapper, converting the provided string to a `Format` and passing it to `printfFmt`. After accepting the format string argument, we parse a `Maybe Format` from it, providing the parsed value to our `PrintfType` function to calculate the rest of our type signature.
+`printf` is easily defined as a simple wrapper, converting the provided string to a `Format` and passing it to `printfFmt`. After accepting the format string argument, we parse a `Maybe Format` from it, providing the parsed value to our `PrintfType` function to calculate the rest of our type signature.
 
 > [!TIP]
 > The `_` syntax that appears in this function introduces an anonymous hole. When the value of a hole is forced by type checking (resolved), the compiler fills in its value for you. Holes defined with `_` will result in an "unsolved holes" compile error if unresolved.
@@ -260,7 +260,7 @@ failing
   runtimeFormatString = printf (blackbox "%s %s") "Hello" "World"
 ```
 
-We can construct a variant of `printf` that will work with runtime format strings by defining a custom, heterogenous list-like structure, and making a fallible version of our `printf` function based on this data structure:
+We can construct a variant of `printf` that will work with runtime format strings by defining a custom, heterogeneous list-like structure, and making a fallible version of our `printf` function based on this data structure:
 
 ```idris
 data PrintfInput : Type where