I had to go to some lengths to make this (associativity of vector append) type check, but it does now… https://gist.github.com/edwinb/dd06af6a2531f7f3bb5cf19f7fb1976d …
-
-
Replying to @edwinbrady
@edwinbrady This is wonderful news! Does it support the whole iterated tower of dependencies or is it purely dreplace?1 reply 0 retweets 0 likes -
Replying to @d_christiansen
@d_christiansen I haven't yet worked out exactly what it works for, so I need to play :). It generates rewriting lemmas for specific types.1 reply 0 retweets 1 like -
-
Replying to @d_christiansen
@d_christiansen Oh, also, if it doesn't work, you can specify your own rewriting lemma as well.1 reply 0 retweets 0 likes -
Replying to @edwinbrady
@edwinbrady excellent! Did you write this in Haskell or Idris? ;-)1 reply 0 retweets 0 likes
Replying to @d_christiansen
@d_christiansen I was very tempted to do this with reflection, but it got fiddly so I wimped out.
10:59 AM - 3 Apr 2016
1 reply
0 retweets
1 like
-
-
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
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.