17 Sep
2014
17 Sep
'14
10:02 a.m.
Use syntax similar to functional dependencies. The injectivity declaration begins with `|` following type family declaration head. `|` is followed by a list of comma-separated injectivity conditions. Each injectivity condition has the form:
{{{ result A -> B }}}
Was `_` considered here as the result token? No, it wasn't.
Also, I think it's best to actually take a look at the wiki as new proposals are being added there. Janek