module Void -- making use of 'hd' being partially definedempty1 : Voidempty1 = hd [] where    hd : List a -> a    hd (x :: xs) = x -- not terminatingempty2 : Voidempty2 = empty2