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!