I’ve done it in Agda - it’s not even hard. The naive definitions are accepted without issue.

https://github.com/mokus0/junkbox/blob/master/Agda/ack.agda