calculational proofs
A calculational proof, or a proof by definition, is one that would be solved with a call to reflexivity in Agda. If we say an equation is true “by definition”, it means that unfolding the definitions calculationally gives two equal expressions to the two sides of the equation.
Tags: mathematics, proof, proof assistants