X-Git-Url: https://git.ralfj.de/web.git/blobdiff_plain/07e5b716718d339a55f7192ae4a0f76e8bba2687..8f3a9b876ae6348f1197da06d9b209337d13f4de:/personal/_posts/2019-05-15-typeclasses-exponential-blowup.md

diff --git a/personal/_posts/2019-05-15-typeclasses-exponential-blowup.md b/personal/_posts/2019-05-15-typeclasses-exponential-blowup.md
index 4c4c0a0..e59917b 100644
--- a/personal/_posts/2019-05-15-typeclasses-exponential-blowup.md
+++ b/personal/_posts/2019-05-15-typeclasses-exponential-blowup.md
@@ -1,6 +1,7 @@
 ---
 title: "Exponential blowup when using unbundled typeclasses to model algebraic hierarchies"
 categories: research coq
+forum: https://coq.discourse.group/t/blog-post-exponential-blowup-when-using-unbundled-typeclasses-to-model-algebraic-hierarchies/289
 ---
 
 When formalizing a proof in an interactive theorem prover like [Coq](https://coq.inria.fr/), one reoccuring issue is the handling of algebraic hierarchies.