1/1: Building Odd (Odd.idr)Main>  0 v : Type 0 k' : Type 0 k : Type   x : k'   y : v   z : List (k', v)-------------------------------------bang : List (k', v)Main> Bye for now!