reg023.idr:7:5:When elaborating right hand side of bad:
Can't unify
        Nat (Type of 0)
with
        f Nat (Expected type)