Publish the new typesafe interpreter post.

content/blog/typesafe_interpreter_revisited.md

@@ -361,7 +361,7 @@ I think this is a good approach. Should we want to add more types to our languag
 lists, and so on, we will be able to extend our `decEq` approach to construct more complex equality
 proofs, and keep the `typecheck` method the same. Had we not used this approach,
 and instead decided to pattern match on types inside of `typecheck`, we would've quickly
-found that this only works for types with finitely many values. When we add polymorphic tuples
+found that this only works for languages with finitely many types. When we add polymorphic tuples
 and lists, we start being able to construct an arbitrary number of types: `[a]`. `[[a]]`, and
 so on. Then, we cease to be able to enumerate all possible pairs of types, and require a recursive
 solution. I think that this leads us back to `decEq`.

content/blog/typesafe_interpreter_tuples.md

@@ -1,8 +1,7 @@
 ---
 title: Meaningfully Typechecking a Language in Idris, With Tuples
-date: 2020-08-11T19:57:26-07:00
+date: 2020-08-12T15:48:04-07:00
 tags: ["Idris"]
-draft: true
 ---
 
 Some time ago, I wrote a post titled