All Questions
2
questions
2
votes
1
answer
152
views
Debug autorewrite in Coq
I often meet proofs using autorewrite which Coq takes a while to process for some reason. (Setoid rewriting)
I then manually figure out which rewrite rules were ...
- 224
1
vote
1
answer
106
views
Proving that applicative functors compose
For simplicity, here an applicative functor means (in a proof assistant based on dependent type theory) the Haskellian applicative functor, bundled with its equational laws.
This I can of course brute ...
- 4,025