Issue2858-invalid.agda:3,1-5,18
No 'constructor' blocks outside of 'interleaved mutual' blocks.
when scope checking the declaration
  constructor
    zero : Nat
    suc : Nat → Nat

———— All done; warnings encountered ————————————————————————

Issue2858-invalid.agda:3,1-5,18
No 'constructor' blocks outside of 'interleaved mutual' blocks.
when scope checking the declaration
  constructor
    zero : Nat
    suc : Nat → Nat
