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 https:

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 https://github.com/mokus0/junkbox/blob/master/Agda/ack.agda