Hi, Rather than trying to find it in the tutorial, I thought I'd ask here about what makes F* unique. I read in Type-Driven Development with Idris that F* uses “refinement types, which are types augmented with a predicate that describes properties of values in that type.” This sounds like what I'm looking for.
Idris can specify the length of a vector, Vect 3 Int, but I don't think it can specify anything about the values of its elements, other than their type (e.g. Int). Can F* specify, in the type, that values in a list output by a function are say 2 more than values in the input list? I'm interested in languages like Idris and F* for their potential application to smart contract development. Will _______________________________________________ fstar-club mailing list fstar-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/fstar-club
