From 7262cce37ab242810e94f3d3a0fe022cdb4e1a25 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 20 Sep 2014 07:44:48 -0700 Subject: [PATCH] fix(doc/lean): typos --- doc/lean/declarations.org | 20 ++++++++++++-------- doc/lean/reducible.org | 10 +++++----- 2 files changed, 17 insertions(+), 13 deletions(-) diff --git a/doc/lean/declarations.org b/doc/lean/declarations.org index a398e3b11..b29a497b2 100644 --- a/doc/lean/declarations.org +++ b/doc/lean/declarations.org @@ -2,14 +2,18 @@ ** Definitions -The command =definition= declares a new constrant/function. The identity function is defined as +The command =definition= declares a new constant/function. The identity function is defined as #+BEGIN_SRC lean definition id (A : Type) (a : A) : A := a #+END_SRC -We say definitions are "transparent", because the type checker can unfold them. The following declaration only type checks because =+= is a transparent definition. -Otherwise, the type checker would reject the expression =v = w= since it would not be able to stablish that =2+3= and =5= are "identical". In Lean, we say they are _definitionally equal_. +We say definitions are "transparent", because the type checker can +unfold them. The following declaration only type checks because =+= is +a transparent definition. Otherwise, the type checker would reject +the expression =v = w= since it would not be able to establish that +=2+3= and =5= are "identical". In type theory, we say they are +_definitionally equal_. #+BEGIN_SRC lean import data.vector data.nat @@ -17,7 +21,7 @@ Otherwise, the type checker would reject the expression =v = w= since it would n check λ (v : vector nat (2+3)) (w : vector nat 5), v = w #+END_SRC -Similarly, the followin definition only type checks because =id= is transparent, and the type checker can stablish that +Similarly, the following definition only type checks because =id= is transparent, and the type checker can establish that =nat= and =id Type nat= are definitionally equal, that is, they are the "same". #+BEGIN_SRC lean @@ -29,12 +33,12 @@ Similarly, the followin definition only type checks because =id= is transparent, ** Theorems In Lean, a theorem is just an =opaque= definition. We usually use -=theorem= for declarating propositions. The idea is that users don't +=theorem= for declaring propositions. The idea is that users don't really care about the actual proof, only about its existence. As described in previous sections, =Prop= (the type of all propositions) is _proof irrelevant_. If we had defined =id= using a theorem the previous example would produce a typing error because the type checker -would be unable to unfold =id= and stablish that =nat= and =id Type +would be unable to unfold =id= and establish that =nat= and =id Type nat= are definitionally equal. ** Opaque definitions @@ -70,7 +74,7 @@ Here is an example id A a -- The following definition is type incorrect. It only type checks if - -- we unfold id, but it is not allowed because the definition is transparent. + -- we unfold id, but it is not allowed because the definition is opaque. /- definition buggy_def (A : Type) (a : A) : Prop := ∀ (b : id Type A), a = b @@ -102,7 +106,7 @@ transparent in this example. ** Private definitions and theorems -Sometimes it is useful to hide auxiliary definitions and theorems form +Sometimes it is useful to hide auxiliary definitions and theorems from the module interface. The keyword =private= allows us to declare local hidden definitions and theorems. A private definition is always opaque. The name of a =private= definition is only visible in the diff --git a/doc/lean/reducible.org b/doc/lean/reducible.org index 8e5602034..7167df52b 100644 --- a/doc/lean/reducible.org +++ b/doc/lean/reducible.org @@ -3,7 +3,7 @@ Lean automation can be configured using different commands and annotations. The =reducible= hint/annotation instructs automation which declarations can be freely unfolded. One of the main components -of the Lean elaborator is a procedure for solving simulateneous +of the Lean elaborator is a procedure for solving simultaneous higher-order unification constraints. Higher-order unification is a undecidable problem. Thus, the procedure implemented in Lean is clearly incomplete, that is, it may fail to find a solution for a set @@ -19,9 +19,9 @@ The higher-order unification procedure has to perform case-analysis. The procedure is essentially implementing a backtracking search. This procedure has to decide whether a definition =C= should be unfolded or not. Here, we roughly divide this decision in two groups: _simple_ -and _complex_. We say a unfolding decision is _simple_ if the +and _complex_. We say an unfolding decision is _simple_ if the procedure does not have to consider an extra case (aka -case-split). That is, it does not increase the search space. We say a +case-split). That is, it does not increase the search space. We say an unfolding decision is _complex_ if it produces at least one extra case, and consequently increases the search space. @@ -30,7 +30,7 @@ We write =reducible(C)= to denote that =C= was marked as reducible by the user, and =irreducible(C)= to denote that =C= was marked as irreducible by the user. Theorems are never unfolded. For a transparent definition =C=, the -higher-order unification procedure uses the following decisition tree. +higher-order unification procedure uses the following decision tree. #+BEGIN_SRC if simple unfolding decision then @@ -88,7 +88,7 @@ modification permanent, and save it in the .olean file. irreducible [persistent] pr2 #+END_SRC -The reducible and irreducible annotations can be removed using the modifer =[none]=. +The reducible and irreducible annotations can be removed using the modifier =[none]=. #+BEGIN_SRC lean definition pr2 (A : Type) (a b : A) : A := b