Proving associativity of my version of concatenation for pointwise predicates (All) on length-indexed lists (Vec) — aka index hell — send help.
Conversation
This Tweet is from a suspended account. Learn more
I had a go at het eq and icong from the stdlib but the recursive call gives me pish, I need to have a better look tomorrow.
1
This Tweet is from a suspended account. Learn more
I already have something similar for nats, although with more granularity (constructors zero, left, right). My foresight is pretty limited, so I'll have a try and see how it goes, thanks for the ideas!
1
This Tweet is from a suspended account. Learn more
1
1
1
