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