🤨
Conversation
This is why people don't like Agda.
1
1
Tbf I'm not even sure this is possible in something like Coq (maybe equations is powerful enough?). It shows the associativity of pointwise proofs on length-indexed vectors by using relations instead of heterogeneous equality
1
2
I just meant the colour scheme.
2
fr tho, it was meant in jest but is probably a bit shitty so I apologise.
2
tbh I wish I knew how to pronounce `|><|` and `><` in my head! But maybe I'm reading this out of context?` 😅
Quote Tweet
Replying to @pigworker
Got something working here. Now to find out whether it's of any use 
github.com/umazalakain/ty
github.com/umazalakain/ty2
It's probably not what you think and I should give it a better name, suggestions welcome