Finish draft of Idris post

content/blog/typesafe_interpreter.md

@@ -1,7 +1,6 @@
 ---
 title: Meaningfully Typechecking a Language in Idris
 date: 2020-02-27T21:58:55-08:00
-draft: true
 tags: ["Haskell", "Idris"]
 ---
 
@@ -253,9 +252,18 @@ Awesome!
 ### Wrapping Up
 In this post, we learned that type checking can be used to translate an expression into
 a more strongly-typed data type, which can be (more) safe to evaluate. To help
-strengthen the types of our expression language, we used the Idris language and
+strengthen the types of
+{{< sidenote "right" "if-else-note" "our expression language," >}}
+You may be thinking, "but where did the if-expressions go?". It turns out
+that making sure that the branches of an if-expression are of the same
+type is actually a fairly difficult task; the best way I found was
+enumerating all the possible "valid" combinations of types in a case-expression.
+Since this is obviously not the right solution, I decided to publish what I have,
+and look for an alternative. If I find a better solution, I will write a follow-up
+post.
+{{< /sidenote >}} we used the Idris language and
 its support for dependent types and Generalized Algebraic Data Types (GADTs).
-I this was interesting!
+I hope this was interesting!
 
 As usual, you can find the code for this post in this website's Git repository. The
 source file we went through today is found [here](https://dev.danilafe.com/Web-Projects/blog-static/src/branch/master/code/typesafe-interpreter/TypesafeIntr.idr).