Three weeks in, and a student hits an ill-typed with abstraction buried in a rewrite. My fault for emphasizing rewrite?
-
-
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.
-
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.
- 1 more reply
New conversation -
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.