Agda-2.3.2.2: test/fail/CoinductiveBuiltinNatural.err
CoinductiveBuiltinNatural.agda:11,21-24 ℕ !=< ∞ ℕ of type Set when checking that the expression suc has type ℕ → ℕ
CoinductiveBuiltinNatural.agda:11,21-24 ℕ !=< ∞ ℕ of type Set when checking that the expression suc has type ℕ → ℕ