[Agda] Re: Erasable vs. irrelevant

[Stefan Monnier]

>> I'm quite confused about these two concepts - as to whether they are
>> the same or not.
> They are not the same.  More stuff is erasable than irrelevant.  This is
> because irrelevance maintains termination of *open* terms, i.e., terms with
> free variables that can have empty types.

Is there a place where those terms are precisely defined (at least in
the context of Agda), BTW?
In the research literature, it seems that various terms (erasure,
irrelevance, implicit) are used, and they don't always refer to the
same thing.


        Stefan