According to Wikipedias article about substructural type-systems, F* support some kind of linear types. Is this true? If so, how? I can't find any information about it in the F* tutorial.
Earlier versions of F* had affine types (closely related to linear types), as described in this paper from 2011: https://www.microsoft.com/en-us/research/publication/secure-distributed-programming-with-value-dependent-types/
However, versions of F* since 2015 dropped affine types in favor of other constructs, notably monadic effects, to model stateful resources.