Mirror of https://github.com/leanprover/lean2 in case it ever disappears
08169c5ac2
Daniel is correct when he says the interaction between choice case-splits, delta case-splits, and coercions can be subtle. I believe the following condition https://github.com/leanprover/lean/blob/master/src/frontends/lean/elaborator.cpp#L111 reduces counter-intuitive behavior. Example, the coercion should not influence the resulting type. BTW, by removing this condition, many files in the library broke when I tried to compile from scratch make clean-olean make I used the following workaround. Given a delta-delta constraint f a =?= f b If the terms are types, and no case-split will be performed, then the delta-delta constraint is eagerly solved. In principle, we don't need the condition that the terms are types. However, many files break if we remove it. The problem is that many files in the standard library are abusing the higher-order unification procedure. The elaboration problems are quite tricky to solve. I use the extra condition "the terms are types" because usually if they are, "f" is morally injective, and we don't really want to unfold it. Note that the following two cases do not work check '{1, 2, 3} check insert 1 (insert 2 (insert 3 empty)) Well, they work if we the num namespace is open, and they are interpreted as having type (finset num) |
||
|---|---|---|
| bin | ||
| doc | ||
| extras/latex | ||
| hott | ||
| images | ||
| library | ||
| script | ||
| src | ||
| tests | ||
| .gitignore | ||
| .travis.osx.yml | ||
| .travis.windows.yml | ||
| .travis.yml | ||
| LICENSE | ||
| README.md | ||
| License | Windows | Ubuntu | OS X | Builds/Tests |
|---|---|---|---|---|
 |
 |
 |
 |
 |
About
- Homepage
- Theorem Proving in Lean: HTML, PDF
- Authors
- Standard Library
- HoTT Library
- Short Tutorial
- To Do list
Requirements
- C++11 compatible compiler: g++ (version >= 4.8.1), or clang++ (version >= 3.3)
- CMake
- GMP (GNU multiprecision library)
- MPFR (GNU MPFR Library)
- Lua 5.2 or 5.1, or LuaJIT 2.0
- (optional) gperftools
- (optional) Boost (version >= 1.54), we can build Lean using boost::thread instead of std::thread. When using Boost, Lean can modify the thread stack size.
Installing required packages at
Windows
Linux
OS X
Build Instructions
Miscellaneous
- Testing and Code Coverage
- Building Doxygen Documentation:
doxygen src/Doxyfile - Coding Style
- Library Style Conventions
- Git Commit Conventions
- Automatic Builds
- Syntax Highlight Lean Code in LaTeX