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.
fstar-club mailing list