Runtime performance for Agda... well, it leaves a lot to be desired, at least with respect to the MAlonzo compiler. For example, operations on the natural numbe

Runtime performance for Agda... well, it leaves a lot to be desired, at least with respect to the MAlonzo compiler. For example, operations on the natural numbers à la Data.Nat get very slow very quickly-- but while the representation used by Data.Bin speeds things up a lot, you just can't do the same Peano-style structural induction on it.