From 03cf9be8b537eeef5235c4a0d803c34f492b2700 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 3 Jan 2014 11:57:41 -0800 Subject: [PATCH] doc(doc/lean/calc.md): link to Nat.lean Signed-off-by: Leonardo de Moura --- doc/lean/calc.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/doc/lean/calc.md b/doc/lean/calc.md index 8a8674aae..5aa42857f 100644 --- a/doc/lean/calc.md +++ b/doc/lean/calc.md @@ -79,4 +79,6 @@ The Lean `let` construct can also be used to build calculational-like proofs. s2 : P a (f (f b)) := Subst s1 (Axf a), s3 : P a b := Subst s2 (Axf b) in s3. -``` \ No newline at end of file +``` + +Finally, the [Nat (natural number) builtin library](../../src/builtin/Nat.lean) makes extensive use of calculational proofs. \ No newline at end of file