Agda-2.3.2.2: test/fail/NaturalAndLevelDifferent.err
NaturalAndLevelDifferent.agda:8,1-26 The argument to BUILTIN LEVEL must be a postulated name when checking the pragma BUILTIN LEVEL ℕ
NaturalAndLevelDifferent.agda:8,1-26 The argument to BUILTIN LEVEL must be a postulated name when checking the pragma BUILTIN LEVEL ℕ