From 17eb2374eece1619b8ab17f0b8a3642ff1d37b60 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 2 Feb 2014 19:14:02 -0800 Subject: [PATCH] doc(README): add link to tutorial in the main page Signed-off-by: Leonardo de Moura --- README.md | 1 + doc/lean/expr.md | 8 ++------ 2 files changed, 3 insertions(+), 6 deletions(-) diff --git a/README.md b/README.md index 4f4df8f451..6159653d07 100644 --- a/README.md +++ b/README.md @@ -17,6 +17,7 @@ About - [Design](doc/design.md) - [To Do list](doc/todo.md) - [Authors](doc/authors.md) +- [Tutorial](doc/lean/tutorial.md) Requirements ------------ diff --git a/doc/lean/expr.md b/doc/lean/expr.md index b3bea51c2b..0c30e15201 100644 --- a/doc/lean/expr.md +++ b/doc/lean/expr.md @@ -23,7 +23,7 @@ check x + y ``` In the following example, we define the constant `s` as the sum of `x` and `y` using the `definition` command. -The `eval` command evaluates (normalizes) the expression `s + 1`. In this example, `eval` will just expand +The `eval` command normalizes the expression `s + 1`. In this example, `eval` will just expand the definition of `s`, and return `x + y + 1`. ```lean @@ -34,19 +34,15 @@ eval s + 1 ## Function applications In Lean, the expression `f t` is a function application, where `f` is a function that is applied to `t`. -In the following example, we define the function `max`. The `eval` command evaluates the application `double 3`, -and returns the value `6`. +We define the function `double` ```lean import tactic -- load basic tactics such as 'simp' definition double (x : Nat) : Nat := x + x -eval double 3 ``` In the following command, we define the function `inc`, and evaluate some expressions using `inc` and `max`. ```lean definition inc (x : Nat) : Nat := x + 1 -eval inc (inc (inc 2)) -eval double (inc 3) ```