>> 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 type of result list has little
connection to source list.
I need either `map` with a stronger type that reflects connection
between the lists or a lemma analogous to `mapElem` from Idris.
Both approaches seem completely doable to me, so we can specify pretty
much any property of list elements. I'm just too lazy to finish the
example. :)


С уважением,
fstar-club mailing list

Reply via email to