Helper Functions

ABSTRACT

This takes a term A and a term B and finds a function f such that f(A)=B. In other words it abstracts the variable A from B and forms a function.

Example:
You can specify whether all the variables A are abstracted or a subset.
Example:
Equvalent to:

Definitional Equality

We compare types using definitional equality, which means that before comparing the types we replace all symbols by their definitions and apply all functions. $$\sqrt{5}$$