packages feed

MiniAgda-0.2014.1.9: test/fail/DottedConstructorsWrong.ma

-- 2013-04-08

data Unit { unit }

fun top : Unit -> Unit
{ top .unit = unit }

data Bool { true ; false }

fail
fun not : Bool -> Bool
{ not .true = false
; not false = true
}

data Nat { zero ; suc (n : Nat) }

fun pred : Nat -> Nat
{ pred zero = zero
; pred (.suc x) = x
}