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>
feat(util/lean_path): add dirname and path_append aux functions

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/module): relative module path

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lean/dependencies): take relative paths into account when computing dependencies

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(library/standard): use relative paths in some files in the standard library

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
test(tests/lean/run): add unicode in identifiers test

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/unifier): add more information in error messages due to type errors when assigning metavariables

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(util/lean_path): workaround 'spurious' warning produced by g++ in release mode

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(util/list): add inline functions for commonly used patterns in list processing code

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/hop_match): port higher-order (pattern) matcher to Lean 0.2, we still have to implement support for universe levels

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/standard/logic/connectives/quantifiers): add some theorems for simplifier

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(tests/lua/hop1): incorrect assertion

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