Post #2728848

There more I think about it, the more excited I become about @jonmsterling 's idea of implementing custom eliminators in Pterodactyl. I was recently working with a binary representation of natural numbers in agda. You can prove these are equivalent to the usual natural numbers and this gives a very useful alternative induction principle that comes from the binary structure. It would be so nice to have a native syntax for this! Currently you have to just apply the function and supply the motive and methods inline. Beside that, there are so many derived universal property type results that this could be useful for. Looking forward to seeing how far you could push this idea.