Idris> *Data\ZZ> *Data\ZZ> *Data\ZZ> *Data\ZZ> Bye bye