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 the compilet 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)
• === 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 yo ~(x == y) (the logical, homogeneous disequality)