Post #3288565

@edwinb @gallais I want to cite the fact that Idris 2 has `Type : Type`. Is there anything more authoritative than the note in the FAQ saying “Idris 2 currently implements Type : Type. Don’t worry, this will not be the case forever!”? (Also, just to be sure: is this note still up to date?)