soonhokong / lean / 904

Builds Branch Commit Type Ran Committer Via Coverage
904 master fix(library/elaborator): in optimization for metavariable free terms The optimization was incorrect if the term indirectly contained a metavariable. It could happen if the term contained a free variable that was assigned in the context to a term ... push leodemoura travis-ci pending completion   set done
903 master feat(library/elaborator): compensate the lack of eta-reduction (and eta-expanded normal forms) in the kernel normalizer Before this commit, the elaborator was solving constraints of the form ctx |- (?m x) == (f x) as ?m <- (fun x :... push leodemoura travis-ci pending completion   set done
902 master feat(builtin/kernel): dependent version of axiom of choice Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> push leodemoura travis-ci pending completion   set done
901 master fix(emacs): syntax highlight Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> push leodemoura travis-ci pending completion   set done
900 master refactor(builtin/kernel): cleanup Hilbert operator definition Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> push leodemoura travis-ci pending completion   set done
898 master feat(builtin/kernel): add Hilbert's operator, and derive axiom of choice using it Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> push leodemoura travis-ci pending completion   set done
897 master chore(library/simplifier): fix style warning Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> push leodemoura travis-ci pending completion   set done
896 master feat(library/simplifier): congruence theorem compilation Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> push leodemoura travis-ci pending completion   set done
895 master feat(library/simplifier): conditional rewriting Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> push leodemoura travis-ci pending completion   set done
894 master test(tests/lua): add test/example that demonstrates how to collect statistics of used theorems Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> push leodemoura travis-ci pending completion   set done
893 master fix(library/expr_lt): use expression depth instead of size to obtain a monotonic total order on terms It is not incorrect to use size, but it can easily overflow due to sharing. The following script demonstrates the problem: local f = Const("f")... push leodemoura travis-ci pending completion   set done
892 master feat(builtin/Nat): flip orientation of associativity axioms for + and * Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> push leodemoura travis-ci pending completion   set done
891 master fix(library/hop_match): style Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> push leodemoura travis-ci pending completion   set done
890 master fix(tests/lean): add expected result file Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> push leodemoura travis-ci pending completion   set done
889 master test(tests/lean): matrix multiplication example Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> push leodemoura travis-ci pending completion   set done