F* symbols reference

Symbols used in F*

This list is incomplete; you can help by expanding it.

Symbol	Explanation
:	type annotation for parameter
::	list cons constructor
<:	type ascription
->	1) function types (can be dependent by naming earlier parameters)
	2) pattern matching, separating pattern from corresponding expression
	3) lambdas, separating arguments from body
|	pattern matching case
;	1) sequencing of stateful code (FIXME: this must desugar, but to what?)
	2) part of lightweight do notation
<--	part of lightweight do notation; x <-- f; y desugars to bind f (fun x -> y) with whatever bind is in context
==	standard library propositional equality type
=	decidable equality, for types that satisfy hasEq
===	"John Major equality", a heterogeneous variant of ==
/\	logical and
\/	logical or
==>	logical implies
<==>	logical iff
~	logical negation
<<	precedes in a well-founded partial order
#	implicit arguments; in 'let f #a x = ...' a will be passed implicitly in calls to f
$	equality constraint for unifier; in val f : $x:int -> y:int -> int, F* will allow any y that is a subtype of int, but x must be exactly of type int
()	single value of type unit. Note that get() is actually a function call of get applied to (), written without spaces to look like a "zero-argument" function call (which F* does not have).
0ul	UInt32.uint_to_t 0 (that is, a UInt32.t literal). The suffixes are the analogous to F# integer literals.
{}	refinement annotation on a type
,	product (tuple) constructor.
*	product (tuple) type. a * b is the type of tuples tuple2 a b.
&	dependent tuple type dtuple2. Similar to sigT in Coq. x:a & p x is the type of tuples dtuple2 a p
(|,|)	dependent tuple constructor.

This list would be best organized by having terse explanations that link to a more complete reference. Currently everything is inline for convenience. When the list is more complete we can reorganize.