Definition
In type theory, definitional equality (or judgmental equality) is a metatheoretic relation between terms of the same type, denoted by the judgment . It represents equality by definition or computational reduction. If two terms are definitionally equal, they are treated as identical by the type-checker.