Agda-2.3.2.2: test/fail/NoNoTerminationCheck.agda
-- Andreas, 2012-03-08
module NoNoTerminationCheck where
{-# NO_TERMINATION_CHECK #-}
f : Set
f = f
-- the pragma should not extend to the following definition
g : Set
g = g
-- error: non-termination