soonhokong / lean / 995

Builds Branch Commit Type Ran Committer Via Coverage
995 master feat(builtin/kernel): prove false_elim without using case Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> push leodemoura travis-ci pending completion   set done
994 version0.2 fix(kernel/diff_cnstrs): missing include Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> push leodemoura travis-ci pending completion   set done
993 version0.2 feat(kernel/level): new universe level datastructure for universe level polymorphism Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> push leodemoura travis-ci pending completion   set done
992 master fix(kernel/type_checker): caching bug Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> push leodemoura travis-ci pending completion   set done
990 master feat(builtin): define list, cons, nil and prove basic theorems Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> push leodemoura travis-ci pending completion   set done
988 master doc(examples/lean): add theorem sent by Jeremy Avigad Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> push leodemoura travis-ci pending completion   set done
987 master doc(examples/lean): proof of concept Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> push leodemoura travis-ci pending completion   set done
986 master doc(examples/lean/abelian): proof of concept Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> push leodemoura travis-ci pending completion   set done
985 master doc(examples/lean/group): prove basic theorems Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> push leodemoura travis-ci pending completion   set done
982 master fix(builtin/num): remove hacks for making the elaborator happy Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> push leodemoura travis-ci pending completion   set done
979 master chore(builtin/num): remove leftover Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> push leodemoura travis-ci pending completion   set done
976 master feat(builtin/num): add auxiliary definitions and theorems for proving the primitive recursion theorem Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> push leodemoura travis-ci pending completion   set done
975 master feat(builtin/num): define lt predicate, and prove basic theorems Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> push leodemoura travis-ci pending completion   set done
974 master doc(todo): update todo list push leodemoura travis-ci pending completion   set done
973 master doc(todo): update todo list push leodemoura travis-ci pending completion   set done