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

Reply via email to