projects
/
web.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(parent:
cf3ce20
)
add forum link
author
Ralf Jung
<post@ralfj.de>
Wed, 15 May 2019 17:48:56 +0000
(19:48 +0200)
committer
Ralf Jung
<post@ralfj.de>
Wed, 15 May 2019 17:48:56 +0000
(19:48 +0200)
personal/_posts/2019-05-15-typeclasses-exponential-blowup.md
patch
|
blob
|
history
diff --git
a/personal/_posts/2019-05-15-typeclasses-exponential-blowup.md
b/personal/_posts/2019-05-15-typeclasses-exponential-blowup.md
index 4c4c0a0ba1bef46472f030520b31d8e8fb206f9a..e59917b87ed92336f88e3925decffd72432179e5 100644
(file)
--- 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.