>> 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. :) Alex. -- С уважением, Александр. _______________________________________________ fstar-club mailing list fstar-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/fstar-club
