CoreNat

Natural-number computation example

Open in Workbench View on GitHub

1-- Natural-number computation example2-- Part of the Grace17 proof assistant for mathematics based on set theory.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Core.Nat8namespace Rec910def add (x y : Nat) -> Nat11  | zero, y => y12  | succ(x), y => succ(add(x, y))1314notation infixl 60 "+" => add1516theorem add.left_unit (y : Nat)17  shows add(0, y) = y18proof19  settle with add2021end Rec22