Agda-2.3.2.2: test/fail/DoNotFireLiteralCatchAllForNeutrals.agda

-- Andreas, 2012-10-09
-- Testcase to ensure we do not fire catch all clause on neutrals in literal matching
module DoNotFireLiteralCatchAllForNeutrals where

postulate String : Set
{-# BUILTIN STRING String #-}

data ⊥ : Set where
record ⊤ : Set where
  constructor trivial

NotNull : String → Set
NotNull "" = ⊥
NotNull s  = ⊤ -- never reduces on open terms

allNull : (s : String) → NotNull s
allNull s = trivial -- should fail

bot : ⊥
bot = allNull ""