Variable Declarations

Q: How can I declare that a variable n is an integer so that, for instance, becomes ?

The simplest way is to use pattern matching with conditional testing. For example:

More elaborate patterns can handle arbitrary expressions.

To demonstrate the validity of the substitution, we can simplify the right hand side using .

For integral , implemented via the substitution , this expression equals .