# Proof software for Primitive Recursive Arithmetic

Primitive Recursive Arithmetic is a critical foundational system in mathematics at large, and all the more so in areas studying constructive reasoning and/or computability such as Theoretical Computer Science.

Is there any proof software that deals with Primitive Recursive Arithmetic... or equivalent systems?

This gives exactly PRA, but in addition, the standard library defines induction up to $\varepsilon_0$, which brings the strength up to full Peano Arithmetic.