Different types of equality in F*

Equalities

F* has 3 different types of equality:

val (=)  : #a:Type{hasEq a} -> a -> a -> Tot bool
val (==) : #a:Type -> a -> a -> Tot Type0
val (===): #a:Type -> #b:Type -> a -> b -> Tot Type0

Here is what each of them means:

• = is boolean equality that is automatically generated by F* for many types with decidable equality; such types satisfy the hasEq predicate. By default every inductive datatype and records have decidable equality generated by F* unless the noeq qualifier has been explicitly set. The standard library also defines the useful alias eqtype as a:Type{hasEq a}.
• == is homogeneous propositional equality, and is defined for all F* types, even the ones without hasEq (== is defined in prims.fst as a squashed inductive and further documented here)
• === is heterogeneous propositional equality; this more exotic equality is sometimes called "John Major equality" (=== is defined in prims.fst as a squashed inductive)

Disequalities

Corresponding to the equalities, there are also the corresponding disequalities :

• x <> y is equivalent to not (x = y) (the decidable boolean valued disequality)
• x =!= y is equivalent to ~(x == y) (the logical, homogeneous disequality)