From 61cdec73f68d5687b423fcce54932f6c57f8ec64 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 6 Mar 2015 14:22:05 -0800
Subject: [PATCH] chore(doc/lean/lexical): remove obsolete documentation from
 Lean 0.1

---
 doc/lean/lexical.md | 74 ---------------------------------------------
 1 file changed, 74 deletions(-)
 delete mode 100644 doc/lean/lexical.md

diff --git a/doc/lean/lexical.md b/doc/lean/lexical.md
deleted file mode 100644
index b8852be95c..0000000000
--- a/doc/lean/lexical.md
+++ /dev/null
@@ -1,74 +0,0 @@
-# Lexical conventions
-
-## Reserved keywords
-
-This is the list of reserved keywords in Lean:
-`axiom`,
-`check`,
-`coercion`,
-`definition`,
-`echo`,
-`environment`,
-`eval`,
-`exit`,
-`have`,
-`help`,
-`import`,
-`infix`,
-`infixr`,
-`infixl`,
-`notation`,
-`options`,
-`pi`,
-`pop::context`,
-`print`,
-`scope`,
-`theorem`,
-`type`,
-`universe`,
-`variable`,
-`variables`,
-`by`,
-`exists`,
-`forall`,
-`fun`,
-`in`,
-`let`
-
-Remark: Lean commands always start with a upper case letter.
-
-The following symbols are also reserved: `->`, `==`, `Π`, `λ`, `→`, `∀`, `∃`, `_`, `,`, `.`, `:`, `(`, `)`, `{`, `}`
-
-## Identifiers
-
-Lean identifiers are divided in 3 categories.
-
-In the first category, identifiers are of the form `[a-zA-Z_'@][a-zA-Z0-9_'@]*`. Here are examples of valid identifiers in this category: `fact`, `sin`, `move_front`, `f1`, `@cast`, and `A'`.
-
-In Lean, we support hierarchical identifiers. A hierarchical is essentially a sequence of category 1 identifiers separated by `::`. We use hierarchical names to simulate modules in Lean. Here are some examples: `mod::x`, `foo::bla::1`.
-
-In the second category, we have any non empty sequence of the following characters: `=`, `<`, `>`, `^`, `|`, `&`, `~`, `+`, `-`, `*`, `/`, `\\`, `$`, `%`, `?`, `;`, `[`, `]`, `#`. Here are examples of indentifiers in this category: `==`, `++`, `<<==`.
-
-In the third category, we have any non empty sequence of non-ascii characters. Here are some examples: `⊆`, `∨`, and `¬`.
-
-This separation may seem adhoc, the main motivation is to minimize the number of white spaces in Lean files.
-For example, we can write `x+y*z` instead of `x + y * z`.
-
-We usually use category 1 identifiers to name variable declarations,
-definitions, axioms and theorems. Category 2 and 3 are usually used to
-define notation, i.e., symbolic abbreviations denoting terms. For
-example, the integer addition is named `Int::add`, and real addition
-`Real::add`.  The symbol `+` is notation for both of them.
-
-## Numerals
-
-Natural numbers are of the form `[0-9]+`, and decimal numbers are of the form `[0-9]+.[0-9]*`.
-Natural numbers have type Nat, and decimal numbers have type Real. Lean automatically introduce coercions when needed.
-
-## Strings
-
-Strings are defined as usual as `"[any sequence of characters excluded "]"`.
-
-## Comments
-
-A comment starts anywhere with a double hyphen `--` and runs until the of the line.