diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean index 2666fe989..61f562a26 100644 --- a/src/builtin/kernel.lean +++ b/src/builtin/kernel.lean @@ -69,6 +69,9 @@ theorem not_intro {a : Bool} (H : a → false) : ¬ a theorem eta {A : TypeU} {B : A → TypeU} (f : ∀ x : A, B x) : (λ x : A, f x) = f := funext (λ x : A, refl (f x)) +-- create default rewrite rule set +(* mk_rewrite_rule_set() *) + theorem trivial : true := refl true diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean index 79e90dd20..321a2daf6 100644 Binary files a/src/builtin/obj/kernel.olean and b/src/builtin/obj/kernel.olean differ diff --git a/src/library/simplifier/simplifier.cpp b/src/library/simplifier/simplifier.cpp index d65aeb8fb..a6b85a8d8 100644 --- a/src/library/simplifier/simplifier.cpp +++ b/src/library/simplifier/simplifier.cpp @@ -133,9 +133,9 @@ class simplifier_fn { match_fn m_match_fn; struct result { - expr m_out; - optional m_proof; - bool m_heq_proof; + expr m_out; // the result of a simplification step + optional m_proof; // a proof that the result is equal to the input (when m_proofs_enabled) + bool m_heq_proof; // true if the proof is for heterogeneous equality explicit result(expr const & out, bool heq_proof = false): m_out(out), m_heq_proof(heq_proof) {} result(expr const & out, expr const & pr, bool heq_proof = false): diff --git a/src/tests/frontends/lean/frontend.cpp b/src/tests/frontends/lean/frontend.cpp index 856129972..17548537b 100644 --- a/src/tests/frontends/lean/frontend.cpp +++ b/src/tests/frontends/lean/frontend.cpp @@ -16,6 +16,7 @@ Author: Leonardo de Moura #include "frontends/lean/frontend.h" #include "frontends/lean/operator_info.h" #include "frontends/lean/pp.h" +#include "frontends/lua/register_modules.h" using namespace lean; static void tst1() { @@ -208,6 +209,7 @@ static void tst11() { int main() { save_stack_info(); + register_modules(); tst1(); tst2(); tst3(); diff --git a/src/tests/frontends/lean/parser.cpp b/src/tests/frontends/lean/parser.cpp index bf9ee80a9..ddba08810 100644 --- a/src/tests/frontends/lean/parser.cpp +++ b/src/tests/frontends/lean/parser.cpp @@ -16,6 +16,7 @@ Author: Leonardo de Moura #include "frontends/lean/parser.h" #include "frontends/lean/frontend.h" #include "frontends/lean/pp.h" +#include "frontends/lua/register_modules.h" using namespace lean; static void parse(environment const & env, io_state const & ios, char const * str) { @@ -109,6 +110,7 @@ static void tst3() { int main() { save_stack_info(); + register_modules(); tst1(); tst2(); tst3(); diff --git a/src/tests/frontends/lean/pp.cpp b/src/tests/frontends/lean/pp.cpp index e8116ada8..c8afb6fd0 100644 --- a/src/tests/frontends/lean/pp.cpp +++ b/src/tests/frontends/lean/pp.cpp @@ -11,6 +11,7 @@ Author: Leonardo de Moura #include "library/io_state_stream.h" #include "frontends/lean/frontend.h" #include "frontends/lean/pp.h" +#include "frontends/lua/register_modules.h" using namespace lean; static expr mk_shared_expr(unsigned depth) { @@ -105,6 +106,7 @@ static void tst6() { int main() { save_stack_info(); + register_modules(); tst1(); tst2(); tst3(); diff --git a/src/tests/kernel/environment.cpp b/src/tests/kernel/environment.cpp index 72b5aa809..786ec3f33 100644 --- a/src/tests/kernel/environment.cpp +++ b/src/tests/kernel/environment.cpp @@ -17,6 +17,7 @@ Author: Leonardo de Moura #include "library/io_state_stream.h" #include "library/arith/arith.h" #include "frontends/lean/frontend.h" +#include "frontends/lua/register_modules.h" using namespace lean; static void tst1() { @@ -272,6 +273,7 @@ static void tst13() { int main() { save_stack_info(); + register_modules(); enable_trace("is_convertible"); tst1(); tst2(); diff --git a/src/tests/kernel/metavar.cpp b/src/tests/kernel/metavar.cpp index 57773b667..e7cbef4ab 100644 --- a/src/tests/kernel/metavar.cpp +++ b/src/tests/kernel/metavar.cpp @@ -24,6 +24,7 @@ Author: Leonardo de Moura #include "library/placeholder.h" #include "library/arith/arith.h" #include "frontends/lean/frontend.h" +#include "frontends/lua/register_modules.h" using namespace lean; static std::ostream & operator<<(std::ostream & out, metavar_env const & menv) { @@ -631,6 +632,7 @@ static void tst28() { int main() { save_stack_info(); + register_modules(); tst1(); tst2(); tst3(); diff --git a/src/tests/kernel/normalizer.cpp b/src/tests/kernel/normalizer.cpp index 2d4479496..2cd4f540a 100644 --- a/src/tests/kernel/normalizer.cpp +++ b/src/tests/kernel/normalizer.cpp @@ -22,6 +22,7 @@ Author: Leonardo de Moura #include "library/deep_copy.h" #include "library/arith/int.h" #include "frontends/lean/frontend.h" +#include "frontends/lua/register_modules.h" using namespace lean; expr normalize(expr const & e) { @@ -344,6 +345,7 @@ static void tst11() { int main() { save_stack_info(); + register_modules(); tst_church_numbers(); tst1(); tst2(); diff --git a/src/tests/kernel/threads.cpp b/src/tests/kernel/threads.cpp index 208dc4de2..9976cc9b7 100644 --- a/src/tests/kernel/threads.cpp +++ b/src/tests/kernel/threads.cpp @@ -16,6 +16,7 @@ Author: Leonardo de Moura #include "library/deep_copy.h" #include "library/arith/arith.h" #include "frontends/lean/frontend.h" +#include "frontends/lua/register_modules.h" using namespace lean; expr norm(expr const & e, environment & env) { @@ -65,6 +66,7 @@ static void tst1() { int main() { save_stack_info(); + register_modules(); tst1(); return 0; } diff --git a/src/tests/kernel/type_checker.cpp b/src/tests/kernel/type_checker.cpp index be662c902..05492ed7f 100644 --- a/src/tests/kernel/type_checker.cpp +++ b/src/tests/kernel/type_checker.cpp @@ -24,6 +24,7 @@ Author: Leonardo de Moura #include "library/io_state_stream.h" #include "library/arith/arith.h" #include "frontends/lean/frontend.h" +#include "frontends/lua/register_modules.h" using namespace lean; expr c(char const * n) { return mk_constant(n); } @@ -488,6 +489,7 @@ static void tst21() { int main() { save_stack_info(); + register_modules(); tst1(); tst2(); tst3(); diff --git a/src/tests/library/arith.cpp b/src/tests/library/arith.cpp index 70e1caac2..979230cc6 100644 --- a/src/tests/library/arith.cpp +++ b/src/tests/library/arith.cpp @@ -13,6 +13,7 @@ Author: Leonardo de Moura #include "library/io_state_stream.h" #include "library/arith/arith.h" #include "frontends/lean/frontend.h" +#include "frontends/lua/register_modules.h" using namespace lean; static void tst0() { @@ -132,6 +133,7 @@ static void tst6() { int main() { save_stack_info(); + register_modules(); tst0(); tst1(); tst2(); diff --git a/src/tests/library/elaborator/elaborator.cpp b/src/tests/library/elaborator/elaborator.cpp index 4a7607020..71e7d74d8 100644 --- a/src/tests/library/elaborator/elaborator.cpp +++ b/src/tests/library/elaborator/elaborator.cpp @@ -18,6 +18,7 @@ Author: Leonardo de Moura #include "library/arith/arith.h" #include "library/elaborator/elaborator.h" #include "frontends/lean/frontend.h" +#include "frontends/lua/register_modules.h" using namespace lean; static void tst1() { @@ -867,6 +868,7 @@ void tst27() { int main() { save_stack_info(); + register_modules(); tst1(); tst2(); tst3(); diff --git a/src/tests/library/tactic/tactic.cpp b/src/tests/library/tactic/tactic.cpp index b5b468b3b..03b1bc67a 100644 --- a/src/tests/library/tactic/tactic.cpp +++ b/src/tests/library/tactic/tactic.cpp @@ -17,6 +17,7 @@ Author: Leonardo de Moura #include "library/tactic/tactic.h" #include "library/tactic/boolean_tactics.h" #include "frontends/lean/frontend.h" +#include "frontends/lua/register_modules.h" using namespace lean; tactic loop_tactic() { @@ -116,6 +117,7 @@ static void tst1() { int main() { save_stack_info(); + register_modules(); tst1(); return has_violations() ? 1 : 0; } diff --git a/tests/lua/simp1.lua b/tests/lua/simp1.lua index 7a13b0b7f..16841d36a 100644 --- a/tests/lua/simp1.lua +++ b/tests/lua/simp1.lua @@ -1,4 +1,3 @@ -mk_rewrite_rule_set() add_rewrite_rules({"Nat", "add_zerol"}) add_rewrite_rules({"Nat", "add_zeror"}) parse_lean_cmds([[