Agda-2.3.2.2: test/fail/BuiltinMustBeConstructor.err
BuiltinMustBeConstructor.agda:12,1-24 suc must be a constructor in the binding to builtin SUC when checking the pragma BUILTIN SUC suc
BuiltinMustBeConstructor.agda:12,1-24 suc must be a constructor in the binding to builtin SUC when checking the pragma BUILTIN SUC suc