The book mentions that = is built into Idris syntax since = is a reserved symbol. Is this the only reason that "Equality in General" is builtin? Are there other pros/cons to having = builtin?
Following listing 8.4 but with an explicit argument, the following seems to work on some simple examples:
data Equal : a > b > Type where
Reflexive : (x : a) > Equal x x
I was also a little surprised to see that b there (after EqNat with two Nats). i.e. a and b can be different types. Is this something to do with heterogenous equality and/or JohnMajor equality (which I've heard of but don't grok yet)?
I also tried the following which worked equally well on my simple examples:
data Equal : a > a > Type where
Reflexive : (x : a) > Equal x x
