Known Bugs in Ecce
If we’ve tripped over it, we put it here. Lacunae in implementation which may lead to bombing with pattern-match failure should also be recorded. Scarcity of round tuits is not a bug: it is a fact of life.
parse⋅print ≠ id
It is not currently the case that everything printed is readable. This problem takes three main forms:
- the parser is insufficiently tolerant of vertical spacing, eg, before or after
=>⇒ ⇒ - fixed? the printer doesn’t bracket enough
- fixed? in any case, we should not be trying to print (s:S):T
Canonicity and Datatypes
The truly intrepid who want to experiment with observational type theory will find that coercions between equal datatypes do not yet compute under constructors. We only have this highly desirable behaviour for the hard wired Boolean and W-types. Watch this space. If you don’t know what I’m talking about, it probably won’t kill you. The usual behaviour of intensional equality survives intact.