Agda-2.3.2.2: test/fail/IrrelevantFin.err
IrrelevantFin.agda:10,33-34 Variable n is declared irrelevant, so it cannot be used here when checking that the expression n has type Nat
IrrelevantFin.agda:10,33-34 Variable n is declared irrelevant, so it cannot be used here when checking that the expression n has type Nat