unary_arithmetic.ipl

Proof assistants often use unary arithmetic: this does not work in IPL as recursive datatypes are not supported. However, unary arithmetic can be approximated using interfaces and procedures.
View file at Google Code.


View file at Google Code.