diff --git a/content/blog/typesafe_interpreter_revisited.md b/content/blog/typesafe_interpreter_revisited.md
index fe38bc7..4a75a99 100644
--- a/content/blog/typesafe_interpreter_revisited.md
+++ b/content/blog/typesafe_interpreter_revisited.md
@@ -8,9 +8,10 @@ tags: ["Idris"]
 Some time ago, I wrote a post titled [Meaningfully Typechecking a Language in Idris]({{< relref "typesafe_interpreter.md" >}}). The gist of the post was as follows:
 
 * _Programming Language Fundamentals_ students were surprised that, despite
-having run their expression through typechecking, they still had to
+having run their expression through (object language) typechecking, they still had to
 have a `Maybe` type in their evaluation functions. This was due to
-the fact that the type system was not certain that typechecking worked.
+the fact that the (meta language) type system was not certain that
+(object language) typechecking worked.
 * A potential solution was to write separate expression types such
 as `ArithExpr` and `BoolExpr`, which are known to produce booleans
 or integers. However, this required the re-implementation of most
@@ -370,4 +371,5 @@ I also hope that I've now redeemed myself as far as logical arguments go. We use
 and made our typechecking function save us from error-checking during evaluation. We did this
 without having to manually create different types of expressions like `ArithExpr` and `BoolExpr`.
 
-That's all I have for today, thank you for reading!
+That's all I have for today, thank you for reading! As always, you can check out the
+[full source code for the typechecker and interpreter](https://dev.danilafe.com/Web-Projects/blog-static/src/branch/master/code/typesafe-interpreter/TypesafeIntrV2.idr) on my Git server.