Different types of equality in F*

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 (https://github.com/FStarLang/FStar/wiki/Deriving-hasEq-predicate-for-inductive-types,-and-types-of-equalities-in-F*).
• == is homogeneous propositional equality, and is defined for all F* types the ones without hasEq
• === is heterogeneous propositional equality; this more exotic equality is sometimes also called "John Major equality"