Symbols and Definitions

A symbol such as \(\pi\) can be manipulated on it's own right, for example: or we can drill down and use it's definition as follows:

Axioms

Axioms are used to create variables of a given type, to create new types or new axiomatic propositions.
For example this creates a new variable, p, of the Prime type. Generally, we should not be doing this! It can be useful for defining new types or axioms. For example we could add an axiom which says that all numbers are bigger than 3 which would clearly break all proofs:

Aliases

We can create a new symbol which is basically an alias for another expression like so (Bug in type when simplified): We can define the notation for it using latex as: We can define a fast evaluator for it: And we can call it as:
Finally we have the automatically created proof that the symbol is equal to it's definition:
We can use it like

Result

We can use result to get the last calculated result: