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/2a0598d090829c0f9db3a7763464d9800d6511dd?hp=38c607cc6b1d382018217f12459685b2ab0d4c22 add forum link --- diff --git a/ralf/_posts/2019-05-15-typeclasses-exponential-blowup.md b/ralf/_posts/2019-05-15-typeclasses-exponential-blowup.md index 4c4c0a0..e59917b 100644 --- a/ralf/_posts/2019-05-15-typeclasses-exponential-blowup.md +++ b/ralf/_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.