fun isNil (t ::: Type) (ls : list t) =
case ls of
Nil => True
| _ => False
fun delist (ls : list string) : xbody =
case ls of
Nil => Nil
| Cons (h, t) => {[h]} :: {delist t}
fun main () = return
{[isNil (Nil : list bool)]},
{[isNil (Cons (1, Nil))]},
{[isNil (Cons ("A", Cons ("B", Nil)))]}
{delist (Cons ("X", Cons ("Y", Cons ("Z", Nil))))}