From 8f3a9b876ae6348f1197da06d9b209337d13f4de Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Wed, 15 May 2019 19:48:56 +0200 Subject: [PATCH 1/1] add forum link --- personal/_posts/2019-05-15-typeclasses-exponential-blowup.md | 1 + 1 file changed, 1 insertion(+) 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. -- 2.30.2