The language of Matita allows the definition of well founded recursive functions over inductive
types; in order to guarantee termination of recursion you are only allowed to make recursive
The language of Matita allows the definition of well founded recursive functions over inductive
types; in order to guarantee termination of recursion you are only allowed to make recursive
Most mathematical functions can be naturally defined in this way. For instance, the sum of two
natural numbers can be defined as follows *)
Most mathematical functions can be naturally defined in this way. For instance, the sum of two
natural numbers can be defined as follows *)