ModuleCompute

Module computation example

Open in Workbench View on GitHub

1-- Module 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.Examples.Compute8import Grace.Core.Nat9open Grace.Core.Nat.Rec1011namespace Demo1213def double (n : Nat) -> Nat14  | zero => zero15  | succ(n) => succ(succ(double(n)))1617theorem double.three (u : Set)18  shows double(3) = 619proof20  simp2122theorem imported_add (u : Set)23  shows add(4, 5) = 924proof25  simp2627end Demo28