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
	3) separator between fields in a record type definition or record constructor
	4) separator between elements in a list literal
<--	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.
{}	1) refinement annotation on a type
	2) record constructor
,	product (tuple) constructor.
*	product (tuple) type. a * b is the type of tuples tuple2 a b.
&	overloaded to construct both dependent and non-dependent tuple types. t1 & t2 is equivalent to tuple2 t1 t2 whereas x:t1 & t2 is dtuple2 t1 (fun x -> t2). See examples/micro-benchmarks/TupleSyntax.fst. The dependent tuple type is similar to sigT in Coq
(|,|)	dependent tuple constructor.
@	list concatenation
^	string concatenation
||	boolean OR
&&	boolean AND
`	quote, transforms an expression into its representation. Read more here.
`@	anti-quotation, inserts an expression of arbitrary type into a quotation. Read more here.
`#	anti-quotation, inserts a term into a quotation. Read more here.
`%	name quotation, replaces a name with the proper string equivalent. It also does name resolution so the length function from FStar.Bytes would be resolved to FStar.Bytes.length. Specifically, `%length would be replaced with "FStar.Bytes.length" at desugaring time.

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.