nicolabotta

I'll play around with a different implementation of `fromInteger` and report. I am actually more worried about the Idris 1 run-time behavior. Shouldn't it be linear in `N`?

It seems plausible that the auto implicit in `fromInteger` is the culprit for the segfaults in Idris 2. The codes ``` > import Data.Fin > import Data.Vect > tail :...

In the specific example, with chicken it takes about twice as long as with chez to compile the `fromNat`case: ``` nicola@cirrus:~/gitlab/botta/Idris2Libs/tests$ time idris2 --cg chicken Linear.idr 1/1: Building Linear (Linear.idr)...

It seems that indexing `Vect n a` with bounded natural numbers instead of `Fin n`s gives a nearly perfect quadratic complexity: ``` import Data.Fin import Data.Vect import Data.Nat LTB :...