I recently stumbled on something called "view", a concept implemented in the Hope language. For those not familiar with it, it let you define bijections between

I recently stumbled on something called "view", a concept implemented in the Hope language. For those not familiar with it, it let you define bijections between 2 different datatypes, so that one may pattern match a piece of data from one datatype with the other datatype constructors, and one of the examples in the paper was precisely that correspondence between peano numbers and usual (unsigned) integers (well, really, it's not quite bijective, given the arch limits on integer representation, but for any purposes we can think of yet, it works). So, the question is: is idris using something like that? Or is there another mechanism? Is it a builtin feature of the language? Do you use the proof system to persuade the language kernel it may translate them back and forth (the "software foundation" book for Coq let the reader build a few proofs about that, though Coq use arbitrary precision numbers iirc))? I'm still quite new on dependent typing, so forgive me if this question is silly or weird somehow.