fix(frontends/lean/scanner): decode utf8

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(kernel/pos_info_provider): get_pos_info return none if position is not available

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean/elaborator): add flyinfo for placeholders

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lean/elaborator): provide type information for expressions using '@' operator, and strict function applications

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lean): flyinfo for identifiers defined in sections

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(util/sexpr/options): typos

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/standard): add markdown documentation
feat(library/standard/logic/axioms): add import default
feat(library/standard/data/nat): port most recent nat to lean 0.2
refactor(library/standard/data/nat): stylistic changes
fix(library/coercion): spurious 'replacing coercion', fixes #22

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean): display warning message when importing file that uses 'sorry'

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean/scanner): allow letter-like unicode characters and sub/super-scripts in identifiers

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/unifier): postpone as much as possible universe constraints of the form ?m1 =?= max(l1, l2) and ?m1 =?= imax(l1, l2) where ?m1 occurs in the right hand side. When there is nothing else to be done, try to solve them by reducing to ?m1 = l1 and ?m1 = l2.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/unifier): when unifier.expensive == true, then use only restrict higher-order unification (a fragment slightly more general than higher-order pattern matching) for solving class-instance constraints

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lean/elaborator): warning message

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lean/scanner): typo reported by clang++

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(README.md): add link to standard library documentation

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/standard/data/option): add basic theorems for option types

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(library/standard/logic/class/decidable): add missing 'end'

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>