formality_core

Module variable

Source

Structs§

CoreBoundVar
Identifies a bound variable.
CoreExistentialVar
CoreUniversalVar
A universal variable is a dummy variable about which nothing is known except that which we see in the environment. When we want to prove something is true for all T (∀T), we replace T with a universal variable.
DebruijnIndex
VarIndex

Enums§

CoreVariable
A term representing a variable.