# Equality

Equality is a subtle issue that pervades the design of all dependent type theories, and F* is no exception. In this first chapter, we briefly touch upon two different kinds of equality in F*, providing some basic information sufficient for the simplest usages. In a subsequent chapter, we’ll cover equality in much greater depth.

## Decidable equality and `eqtype`

We’ve implicitly used the equality operator `=` already (e.g., when defining `factorial`). This is the boolean equality operator. Given two terms `e₁ : t` and `e₂ : t`, so long as `t` supports a notion of decidable equality, `(e₁ = e₂) : bool`.

To see why not all types support decidably equality, consider `t` to be a function type, like `int -> int`. To decide if two functions `f₁, f₂ : int -> int` are equal, we’d have to apply them to all the infinitely many integers and compare their results—clearly, this is not decidable.

The type `eqtype` is the type of types that support decidably equality. That is, given `e₁ : t` and `e₂ : t`, it is only permissible to compare `e₁ = e₂` if `t : eqtype`.

For any type definition, F* automatically computes whether or not that type is an `eqtype`. We’ll explain later exactly how F* decides whether or not a type is an `eqtype`. Roughly, for F* has built-in knowledge that various primitive types like integers and booleans support decidable equality. When defining a new type, F* checks to that all values of the the new type are composed structurally of terms that support decidable equality. In particular, if an `e : t` may contain a sub-term that is a function, then `t` cannot be an `eqtype`.

As such, the type of the decidable equality operator is

```val ( = ) (#a:eqtype) (x:a) (y:a) : bool
```

That is, `x = y` is well-typed only when `x : a` and `y : a` and `a : eqtype`.

Note

We see here a bit of F* syntax for defining infix operators. Rather than only using the `val` or `let` notation with alphanumeric identifiers, the notation `( = )` introduces an infix operator defined with non-alphanumeric symbols. You can read more about this here.

## Propositional equality

F* offers another notion of equality, propositional equality, written `==`. For any type `t`, given terms `e₁, e₂ : t`, the proposition `e₁ == e₂` asserts the (possibly undecidable) equality of `e₁` and `e₂`. The type of the propositional equality operator is shown below:

```val ( == ) (#a:Type) (x:a) (y:a) : prop
```

Unlike decidable equality `(=)`, propositional equality is defined for all types. The result type of `(==)` is `prop`, the type of propositions. We’ll learn more about that in the next chapter.