From: Ralf Jung Date: Wed, 15 May 2019 17:48:56 +0000 (+0200) Subject: add forum link X-Git-Url: https://git.ralfj.de/web.git/commitdiff_plain/fc954d7e5d5fdec603552babba280899ed82fc4a add forum link --- 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.