Lean (証明アシスタント)
自然数は帰納型(英語版)として定義することができる。この定義はペアノの公理に基づいており、すべての自然数はゼロもしくは他の自然数の後者であると述べている。
自然数の加算はパターン・マッチングを使用して、再帰的定義することも可能。
これはLeanのtermモードでの簡単な証明である。
これと同じ証明は戦略を駆使して達成できる。