soonhokong / lean / 972

Builds Branch Commit Type Ran Committer Via Coverage
972 master chore(builtin/num): update object file Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> push leodemoura travis-ci pending completion   set done
971 master feat(builtin): add num type (the base type that will be used to build nat, int, real) Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> push leodemoura travis-ci pending completion   set done
970 master fix(library/elaborator): fix glitches in the elaborator that were forcing us to provide parameters explicitly Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> push leodemoura travis-ci pending completion   set done
969 master doc(todo): remove item from todo list Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> push leodemoura travis-ci pending completion   set done
968 master chore(builtin/sum): cleanup Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> push leodemoura travis-ci pending completion   set done
967 master feat(library/elaborator): be 'lazy' when normalizing terms in the elaborator Unification constraints of the form ctx |- ?m[inst:i v] == T and ctx |- (?m a1 ... an) == T are delayed by elaborator because the produce ... push leodemoura travis-ci pending completion   set done
966 master chore(frontends/lean/parser): update comments Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> push leodemoura travis-ci pending completion   set done
965 master doc(todo): add another item to todo list push leodemoura travis-ci pending completion   set done
964 master fix(frontends/lean): import explicit versions when using the command 'using' Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> push leodemoura travis-ci pending completion   set done
963 master feat(frontends/lean/pp): change how lift local entries are pretty printed Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> push leodemoura travis-ci pending completion   set done
962 master doc(todo): update todo list push leodemoura travis-ci pending completion   set done
961 master fix(library/elaborator): try first projection before imitation in the higher-order unifier Projections build more general solutions. This commit also adds a test that demonstrates the issue. Before this commit, the elaborator would produce the "c... push leodemoura travis-ci pending completion   set done
960 master test(tests/lean): test super opaque style Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> push leodemoura travis-ci pending completion   set done
959 master chore(build): fix build dependencies Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> push leodemoura travis-ci pending completion   set done
958 master refactor(builtin): move pair definition and theorems to pair.lean Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> push leodemoura travis-ci pending completion   set done