Agda-2.3.2.2: test/fail/MatchOnIrrelevantData1.err
MatchOnIrrelevantData1.agda:17,1-18,43 Cannot split on argument of irrelevant datatype Fin @0 when checking the definition of toNat
MatchOnIrrelevantData1.agda:17,1-18,43 Cannot split on argument of irrelevant datatype Fin @0 when checking the definition of toNat