Three weeks in, and a student hits an ill-typed with abstraction buried in a rewrite. My fault for emphasizing rewrite?
-
-
Replying to @plragde
As time goes, I have become less and less enamoured with rewrite. But some of that is because of the kind of stuff I'm using Agda for, and rewrite doesn't let me generalize easily to weak settings. If I was working with irrelevant proofs, I'd use rewrite.
1 reply 0 retweets 0 likes -
Replying to @jjcarett2 @plragde
I spent most of the weekend fixing performance issues with Idris 2, all of which turned out to be due to its take on rewrite... I find the need to use it often indicates I need to think harder about the types I'm working with.
1 reply 0 retweets 2 likes -
Replying to @edwinbrady @jjcarett2
This arose because I asked them to prove an isomorphism between a datatype and a dependent pair type. One component involves proving two dependent pair expressions equal.
2 replies 0 retweets 0 likes
Probably hard to avoid in that case then!
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.