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 -
There are theorems available to rewrite each component of the pair, but you can't apply them one at a time! And I know the fix, but I'm not entirely sure why it's a fix.
2 replies 0 retweets 0 likes -
Replying to @plragde @edwinbrady
There's a dependent cong that's often useful in such situations. Not sure if it's in the standard library yet.
2 replies 0 retweets 0 likes
The issue I was wrestling with was that the type was really big. Not sure it would have helped. I'd like to say to users "Don't Do That Then" but that is cheating somehow.
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.