Issue578.agda

-- 2012-03-06 Andreas
-- Errors during printing of debug messages should not propagate to the
-- top level

{-# OPTIONS -v tc.meta.assign:10 #-}
module Issue578 where

-- Skipping import of Level will leave us with no level builtins
-- import Level

data D : Set where

-- This will generate a debug message, but it cannot be printed
-- since there are no bindings for the level builtins.

-- However, the file should still succeed.