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