packages feed

MiniAgda-0.2014.1.9: test/fail/incompleteSizePattern1.ma

data Empty : Set
{
}

-- recursion on Size fails since ($ i) is not a complete pattern match
cofun bad' : Size -> Empty
{
  bad' ($ i) = bad' _
}