[Agda] Re: Erasable vs. irrelevant

Stefan Monnier monnier at iro.umontreal.ca
Sat Jan 21 05:48:02 CET 2012

>> 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.


More information about the Agda mailing list