>> Unfortunately, this particular code doesn't work, most likely I
>> should've formulated it differently.
>
> You're just missing an open FStar.Mul, AFAICT :)
Yeah, that helped up to a point. :)
After that I stumbled upon (kinda expected) issue that `map` "looses"
type information in a sense the
Hi Will,
Actually, both Idris (and any Dependently-Typed language) and F* (or
LiquidHaskell for that matter) can express properties of elements. I
implemented your example in Idris, it goes like this:
```
module Example
import Data.Vect
ix2 : Int -> Int
ix2 i = i*2
foo : {n: Nat} -> (l: Vect n
