From 3d9b557cfd3d64973c0f5cc0654cff52584fd780 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 12 Jun 2015 17:32:18 -0700 Subject: [PATCH] feat(frontends/lean): allow the user to mark subterms that should be automatically abstracted into new definitions closes #484 --- src/emacs/lean-syntax.el | 2 +- src/frontends/lean/CMakeLists.txt | 2 +- src/frontends/lean/builtin_exprs.cpp | 2 + src/frontends/lean/decl_attributes.cpp | 16 ++ src/frontends/lean/decl_attributes.h | 2 + src/frontends/lean/decl_cmds.cpp | 25 ++- src/frontends/lean/elaborator.cpp | 1 + src/frontends/lean/init_module.cpp | 3 + src/frontends/lean/nested_declaration.cpp | 221 ++++++++++++++++++++++ src/frontends/lean/nested_declaration.h | 24 +++ src/frontends/lean/token_table.cpp | 2 +- tests/lean/nested1.lean | 19 ++ tests/lean/nested1.lean.expected.out | 8 + tests/lean/nested2.lean | 32 ++++ tests/lean/nested2.lean.expected.out | 15 ++ 15 files changed, 366 insertions(+), 8 deletions(-) create mode 100644 src/frontends/lean/nested_declaration.cpp create mode 100644 src/frontends/lean/nested_declaration.h create mode 100644 tests/lean/nested1.lean create mode 100644 tests/lean/nested1.lean.expected.out create mode 100644 tests/lean/nested2.lean create mode 100644 tests/lean/nested2.lean.expected.out diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index 9451f12f6..f62789c85 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -11,7 +11,7 @@ '("import" "prelude" "tactic_hint" "protected" "private" "definition" "renaming" "hiding" "exposing" "parameter" "parameters" "begin" "begin+" "proof" "qed" "conjecture" "constant" "constants" "hypothesis" "lemma" "corollary" "variable" "variables" "premise" "premises" - "print" "theorem" "example" "abbreviation" + "print" "theorem" "example" "abbreviation" "abstract" "open" "as" "export" "override" "axiom" "axioms" "inductive" "with" "structure" "record" "universe" "universes" "alias" "help" "environment" "options" "precedence" "reserve" "match" "infix" "infixl" "infixr" "notation" "postfix" "prefix" diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt index c7444fd60..d7e2d49df 100644 --- a/src/frontends/lean/CMakeLists.txt +++ b/src/frontends/lean/CMakeLists.txt @@ -9,6 +9,6 @@ coercion_elaborator.cpp info_tactic.cpp init_module.cpp elaborator_context.cpp calc_proof_elaborator.cpp parse_tactic_location.cpp parse_rewrite_tactic.cpp builtin_tactics.cpp type_util.cpp elaborator_exception.cpp migrate_cmd.cpp local_ref_info.cpp -obtain_expr.cpp decl_attributes.cpp) +obtain_expr.cpp decl_attributes.cpp nested_declaration.cpp) target_link_libraries(lean_frontend ${LEAN_LIBS}) diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 6e5754c32..723e2c7aa 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -33,6 +33,7 @@ Author: Leonardo de Moura #include "frontends/lean/info_annotation.h" #include "frontends/lean/structure_cmd.h" #include "frontends/lean/obtain_expr.h" +#include "frontends/lean/nested_declaration.h" namespace lean { namespace notation { @@ -626,6 +627,7 @@ parse_table init_nud_table() { r = r.add({transition("assert", mk_ext_action(parse_assert))}, x0); r = r.add({transition("show", mk_ext_action(parse_show))}, x0); r = r.add({transition("obtain", mk_ext_action(parse_obtain))}, x0); + r = r.add({transition("abstract", mk_ext_action(parse_nested_declaration))}, x0); r = r.add({transition("if", mk_ext_action(parse_if_then_else))}, x0); r = r.add({transition("(", Expr), transition(")", mk_ext_action(parse_rparen))}, x0); r = r.add({transition("(", Expr), transition(":", Expr), transition(")", mk_ext_action(parse_typed_expr))}, x0); diff --git a/src/frontends/lean/decl_attributes.cpp b/src/frontends/lean/decl_attributes.cpp index d9b25e280..f05fe22c0 100644 --- a/src/frontends/lean/decl_attributes.cpp +++ b/src/frontends/lean/decl_attributes.cpp @@ -246,4 +246,20 @@ environment decl_attributes::apply(environment env, io_state const & ios, name c env = mark_multiple_instances(env, d, m_persistent); return env; } + +void decl_attributes::write(serializer & s) const { + s << m_def_only << m_is_abbrev << m_persistent << m_is_instance << m_is_coercion + << m_is_reducible << m_is_irreducible << m_is_semireducible << m_is_quasireducible + << m_is_class << m_is_parsing_only << m_has_multiple_instances << m_unfold_f_hint + << m_constructor_hint << m_symm << m_trans << m_refl << m_subst << m_recursor + << m_rewrite << m_recursor_major_pos << m_priority << m_unfold_c_hint; +} + +void decl_attributes::read(deserializer & d) { + d >> m_def_only >> m_is_abbrev >> m_persistent >> m_is_instance >> m_is_coercion + >> m_is_reducible >> m_is_irreducible >> m_is_semireducible >> m_is_quasireducible + >> m_is_class >> m_is_parsing_only >> m_has_multiple_instances >> m_unfold_f_hint + >> m_constructor_hint >> m_symm >> m_trans >> m_refl >> m_subst >> m_recursor + >> m_rewrite >> m_recursor_major_pos >> m_priority >> m_unfold_c_hint; +} } diff --git a/src/frontends/lean/decl_attributes.h b/src/frontends/lean/decl_attributes.h index 6657f76a6..888d79f51 100644 --- a/src/frontends/lean/decl_attributes.h +++ b/src/frontends/lean/decl_attributes.h @@ -43,5 +43,7 @@ public: void parse(parser & p); environment apply(environment env, io_state const & ios, name const & d) const; bool is_parsing_only() const { return m_is_parsing_only; } + void write(serializer & s) const; + void read(deserializer & d); }; } diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index 504741b14..48c3c2a7e 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -27,6 +27,7 @@ Author: Leonardo de Moura #include "frontends/lean/tokens.h" #include "frontends/lean/decl_attributes.h" #include "frontends/lean/update_environment_exception.h" +#include "frontends/lean/nested_declaration.h" namespace lean { static environment declare_universe(parser & p, environment env, name const & n, bool local) { @@ -671,6 +672,12 @@ class definition_cmd_fn { m_name = m_p.check_id_next("invalid declaration, identifier expected"); } + expr extract_nested(expr const & v) { + expr new_v; + std::tie(m_env, new_v) = extract_nested_declarations(m_env, m_p.ios(), m_name, v); + return new_v; + } + void parse_type_value() { // Parse universe parameters parser::local_scope scope1(m_p); @@ -690,6 +697,7 @@ class definition_cmd_fn { m_type = m_p.parse_expr(); save_checkpoint(); if (is_curr_with_or_comma_or_bar(m_p)) { + allow_nested_decls_scope scope2(is_definition()); m_value = parse_equations(m_p, m_name, m_type, m_aux_decls, optional(), buffer(), m_pos); } else if (!is_definition() && !m_p.curr_is_token(get_assign_tk())) { @@ -697,6 +705,7 @@ class definition_cmd_fn { m_value = m_p.save_pos(mk_expr_placeholder(), pos); } else { m_p.check_token_next(get_assign_tk(), "invalid declaration, ':=' expected"); + allow_nested_decls_scope scope2(is_definition()); m_value = m_p.save_pos(m_p.parse_expr(), pos); } } else { @@ -711,11 +720,13 @@ class definition_cmd_fn { m_type = Pi(ps, type, m_p); save_checkpoint(); if (is_curr_with_or_comma_or_bar(m_p)) { + allow_nested_decls_scope scope2(is_definition()); m_value = parse_equations(m_p, m_name, type, m_aux_decls, lenv, ps, m_pos); } else if (!is_definition() && !m_p.curr_is_token(get_assign_tk())) { check_end_of_theorem(m_p); m_value = m_p.save_pos(mk_expr_placeholder(), pos); } else { + allow_nested_decls_scope scope2(is_definition()); m_p.check_token_next(get_assign_tk(), "invalid declaration, ':=' expected"); m_value = m_p.parse_scoped_expr(ps, *lenv); } @@ -730,6 +741,7 @@ class definition_cmd_fn { m_type = Pi(ps, m_type, m_p); save_checkpoint(); m_p.check_token_next(get_assign_tk(), "invalid declaration, ':=' expected"); + allow_nested_decls_scope scope2(is_definition()); m_value = m_p.parse_scoped_expr(ps, *lenv); } erase_local_binder_info(ps); @@ -837,6 +849,7 @@ class definition_cmd_fn { cd = check(mk_axiom(m_real_name, c_ls, c_type)); m_env = module::add(m_env, *cd); } else { + c_value = extract_nested(c_value); cd = check(mk_definition(m_env, m_real_name, c_ls, c_type, c_value)); if (!m_is_private) m_p.add_decl_index(m_real_name, m_pos, m_p.get_cmd_token(), c_type); @@ -947,7 +960,7 @@ class definition_cmd_fn { if (aux_values.size() != m_real_aux_names.size()) throw exception("invalid declaration, failed to compile auxiliary declarations"); m_type = postprocess(m_env, m_type); - m_value = postprocess(m_env, m_value); + m_value = extract_nested(postprocess(m_env, m_value)); for (unsigned i = 0; i < aux_values.size(); i++) { m_aux_types[i] = postprocess(m_env, m_aux_types[i]); aux_values[i] = postprocess(m_env, aux_values[i]); @@ -1005,10 +1018,12 @@ class definition_cmd_fn { } } else { std::tie(m_type, m_value, new_ls) = elaborate_definition(m_type, m_value); - new_ls = append(m_ls, new_ls); - m_type = postprocess(m_env, m_type); - m_value = postprocess(m_env, m_value); - m_env = module::add(m_env, check(mk_definition(m_env, m_real_name, new_ls, m_type, m_value))); + new_ls = append(m_ls, new_ls); + m_type = postprocess(m_env, m_type); + m_value = postprocess(m_env, m_value); + expr new_val = extract_nested(m_value); + m_env = module::add(m_env, check(mk_definition(m_env, m_real_name, new_ls, m_type, new_val))); + // Remark: we cache the definition with the nested declarations. m_p.cache_definition(m_real_name, pre_type, pre_value, new_ls, m_type, m_value); } } diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 363565c0b..5b948ab5c 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -52,6 +52,7 @@ Author: Leonardo de Moura #include "frontends/lean/info_tactic.h" #include "frontends/lean/begin_end_ext.h" #include "frontends/lean/elaborator_exception.h" +#include "frontends/lean/nested_declaration.h" #include "frontends/lean/calc.h" #include "frontends/lean/decl_cmds.h" diff --git a/src/frontends/lean/init_module.cpp b/src/frontends/lean/init_module.cpp index aa1a9fb60..e992c789e 100644 --- a/src/frontends/lean/init_module.cpp +++ b/src/frontends/lean/init_module.cpp @@ -31,6 +31,7 @@ Author: Leonardo de Moura #include "frontends/lean/local_ref_info.h" #include "frontends/lean/obtain_expr.h" #include "frontends/lean/decl_cmds.h" +#include "frontends/lean/nested_declaration.h" namespace lean { void initialize_frontend_lean_module() { @@ -61,8 +62,10 @@ void initialize_frontend_lean_module() { initialize_local_ref_info(); initialize_obtain_expr(); initialize_decl_cmds(); + initialize_nested_declaration(); } void finalize_frontend_lean_module() { + finalize_nested_declaration(); finalize_decl_cmds(); finalize_obtain_expr(); finalize_local_ref_info(); diff --git a/src/frontends/lean/nested_declaration.cpp b/src/frontends/lean/nested_declaration.cpp new file mode 100644 index 000000000..eae2cdade --- /dev/null +++ b/src/frontends/lean/nested_declaration.cpp @@ -0,0 +1,221 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include +#include "util/sstream.h" +#include "kernel/type_checker.h" +#include "kernel/find_fn.h" +#include "kernel/instantiate.h" +#include "kernel/abstract.h" +#include "library/locals.h" +#include "library/scoped_ext.h" +#include "library/kernel_serializer.h" +#include "library/replace_visitor.h" +#include "library/module.h" +#include "library/aliases.h" +#include "frontends/lean/decl_attributes.h" +#include "frontends/lean/tokens.h" +#include "frontends/lean/parser.h" +#include "frontends/lean/util.h" +#include "frontends/lean/nested_declaration.h" + +namespace lean { +static name * g_nested_decl = nullptr; +static std::string * g_nested_decl_opcode = nullptr; + +name const & get_nested_decl_name() { return *g_nested_decl; } +std::string const & get_nested_decl_opcode() { return *g_nested_decl_opcode; } + +class nested_decl_macro_definition_cell : public macro_definition_cell { + optional m_name; + decl_attributes m_attributes; + + void check_macro(expr const & m) const { + if (!is_macro(m) || macro_num_args(m) != 1) + throw exception(sstream() << "invalid nested declaration, incorrect number of arguments"); + } +public: + nested_decl_macro_definition_cell(optional const & n, decl_attributes const & attrs): + m_name(n), m_attributes(attrs) {} + virtual name get_name() const { return get_nested_decl_name(); } + virtual pair check_type(expr const & m, extension_context & ctx, bool infer_only) const { + check_macro(m); + return ctx.check_type(macro_arg(m, 0), infer_only); + } + virtual optional expand(expr const & m, extension_context &) const { + check_macro(m); + return some_expr(macro_arg(m, 0)); + } + virtual void write(serializer & s) const { + s.write_string(get_nested_decl_opcode()); + s << m_name; + m_attributes.write(s); + } + virtual unsigned hash() const { + return get_nested_decl_name().hash(); + } + optional const & get_decl_name() const { return m_name; } + decl_attributes const & get_decl_attributes() const { return m_attributes; } +}; + +expr mk_nested_declaration(optional const & n, decl_attributes const & attrs, expr const & e) { + macro_definition def(new nested_decl_macro_definition_cell(n, attrs)); + return mk_macro(def, 1, &e); +} + +bool is_nested_declaration(expr const & e) { + return is_macro(e) && macro_def(e).get_name() == get_nested_decl_name(); +} + +expr update_nested_declaration(expr const & e, expr const & new_d) { + lean_assert(is_nested_declaration(e)); + return mk_macro(macro_def(e), 1, &new_d); +} + +expr get_nested_declaration_arg(expr const & e) { + lean_assert(is_nested_declaration(e)); + return macro_arg(e, 0); +} + +optional const & get_nested_declaration_name(expr const & d) { + lean_assert(is_nested_declaration(e)); + return static_cast(macro_def(d).raw())->get_decl_name(); +} + +decl_attributes const & get_nested_declaration_attributes(expr const & d) { + lean_assert(is_nested_declaration(e)); + return static_cast(macro_def(d).raw())->get_decl_attributes(); +} + +LEAN_THREAD_VALUE(bool, g_allow_nested_declarations, false); + +allow_nested_decls_scope::allow_nested_decls_scope(bool enable) { + m_saved = g_allow_nested_declarations; + g_allow_nested_declarations = enable; +} + +allow_nested_decls_scope::~allow_nested_decls_scope() { + g_allow_nested_declarations = m_saved; +} + +expr parse_nested_declaration(parser & p, unsigned, expr const *, pos_info const & pos) { + try { + optional n; + decl_attributes attrs; + if (!g_allow_nested_declarations) + throw parser_error("invalid 'abstract' expression, it is only allowed inside definitions", pos); + if (p.curr_is_token(get_as_tk())) { + p.next(); + n = p.check_id_next("invalid 'abstract' expression, identifier expected"); + } + attrs.parse(p); + expr e = p.parse_expr(); + p.check_token_next(get_end_tk(), "invalid 'abstract' expression, 'end' expected"); + return p.save_pos(mk_nested_declaration(n, attrs, e), pos); + } catch (exception & ex) { + consume_until_end(p); + ex.rethrow(); + lean_unreachable(); + } +} + +bool contains_nested_declarations(expr const & e) { + return static_cast(find(e, [&](expr const & n, unsigned) { return is_nested_declaration(n); })); +} + +class extractor : public replace_visitor { + environment m_env; + io_state m_ios; + type_checker m_tc; + name m_dname; + unsigned m_idx; +public: + extractor(environment const & env, io_state const & ios, name const & dname): + m_env(env), m_ios(ios), m_tc(m_env), m_dname(dname), m_idx(1) {} + + name mk_name_for(expr const & e) { + lean_assert(is_nested_declaration(e)); + if (auto n = get_nested_declaration_name(e)) { + return *n; + } else { + name ns = get_namespace(m_env); + while (true) { + name aux = m_dname.append_after(m_idx); + m_idx++; + if (!m_env.find(ns + aux)) + return aux; + } + } + } + + expr extract(expr const & e) { + lean_assert(is_nested_declaration(e)); + expr const & d = visit(get_nested_declaration_arg(e)); + name new_name = mk_name_for(e); + name new_real_name = get_namespace(m_env) + new_name; + collected_locals locals; + collect_locals(d, locals); + buffer uparams; + collect_univ_params(d).to_buffer(uparams); + expr new_value = Fun(locals.get_collected(), d); + expr new_type = m_tc.infer(new_value).first; + level_param_names new_ps = to_list(uparams); + levels ls = param_names_to_levels(new_ps); + m_env = module::add(m_env, check(m_env, mk_definition(m_env, new_real_name, new_ps, + new_type, new_value))); + if (new_name != new_real_name) + m_env = add_expr_alias_rec(m_env, new_name, new_real_name); + decl_attributes const & attrs = get_nested_declaration_attributes(e); + m_env = attrs.apply(m_env, m_ios, new_real_name); + return mk_app(mk_constant(new_real_name, ls), locals.get_collected()); + } + + expr visit_macro(expr const & e) { + if (is_nested_declaration(e)) { + return extract(e); + } else { + return replace_visitor::visit_macro(e); + } + } + + expr visit_binding(expr const & b) { + expr new_domain = visit(binding_domain(b)); + expr l = mk_local(m_tc.mk_fresh_name(), new_domain); + expr new_body = abstract(visit(instantiate(binding_body(b), l)), l); + return update_binding(b, new_domain, new_body); + } + + environment const & get_env() const { return m_env; } +}; + +std::tuple extract_nested_declarations(environment const & env, io_state const & ios, + name const & dname, expr const & e) { + if (contains_nested_declarations(e)) { + extractor ex(env, ios, dname); + expr new_e = ex(e); + return std::make_tuple(ex.get_env(), new_e); + } else { + return std::make_tuple(env, e); + } +} + +void initialize_nested_declaration() { + g_nested_decl = new name("nested_decl"); + g_nested_decl_opcode = new std::string("NDecl"); + register_macro_deserializer(get_nested_decl_opcode(), + [](deserializer & d, unsigned num, expr const * args) { + if (num != 1) + throw corrupted_stream_exception(); + optional n; decl_attributes attrs; + d >> n; attrs.read(d); + return mk_nested_declaration(n, attrs, args[0]); + }); +} +void finalize_nested_declaration() { + delete g_nested_decl; + delete g_nested_decl_opcode; +} +} diff --git a/src/frontends/lean/nested_declaration.h b/src/frontends/lean/nested_declaration.h new file mode 100644 index 000000000..4ade145d2 --- /dev/null +++ b/src/frontends/lean/nested_declaration.h @@ -0,0 +1,24 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "util/flet.h" +#include "kernel/expr.h" +namespace lean { +class parser; +// auxiliary object used to temporarily enable nested declarations +class allow_nested_decls_scope { + bool m_saved; +public: + allow_nested_decls_scope(bool enable = true); + ~allow_nested_decls_scope(); +}; +expr parse_nested_declaration(parser & p, unsigned, expr const *, pos_info const & pos); +std::tuple extract_nested_declarations(environment const & env, io_state const & ios, + name const & def_name, expr const & e); +void initialize_nested_declaration(); +void finalize_nested_declaration(); +} diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index f0fa03b87..6a529b1d7 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -97,7 +97,7 @@ void init_token_table(token_table & t) { {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {"rewrite", 0}, {"xrewrite", 0}, {"krewrite", 0}, {"esimp", 0}, {"fold", 0}, {"unfold", 0}, {"generalize", 0}, {"as", 0}, {":=", 0}, {"--", 0}, {"#", 0}, - {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"begin+", g_max_prec}, + {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"begin+", g_max_prec}, {"abstract", g_max_prec}, {"proof", g_max_prec}, {"qed", 0}, {"@", g_max_prec}, {"sorry", g_max_prec}, {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {"?(", g_max_prec}, {"⌞", g_max_prec}, {"⌟", 0}, {"match", 0}, diff --git a/tests/lean/nested1.lean b/tests/lean/nested1.lean new file mode 100644 index 000000000..050763629 --- /dev/null +++ b/tests/lean/nested1.lean @@ -0,0 +1,19 @@ +import data.nat +open nat + +namespace test + +constant foo (a : nat) : a > 0 → nat + +definition bla (a : nat) := +foo + (succ (succ a)) + abstract as foo.prf [irreducible] lt.step (zero_lt_succ a) end + +print foo.prf +print bla + +end test + +print test.bla +print test.foo.prf diff --git a/tests/lean/nested1.lean.expected.out b/tests/lean/nested1.lean.expected.out new file mode 100644 index 000000000..732b9debf --- /dev/null +++ b/tests/lean/nested1.lean.expected.out @@ -0,0 +1,8 @@ +definition test.foo.prf [irreducible] : ∀ (x : ℕ), 0 < succ (succ x) +λ (x : ℕ), lt.step (zero_lt_succ x) +definition test.bla : ℕ → ℕ +λ (a : ℕ), foo (succ (succ a)) (foo.prf a) +definition test.bla : ℕ → ℕ +λ (a : ℕ), test.foo (succ (succ a)) (test.foo.prf a) +definition test.foo.prf : ∀ (x : ℕ), 0 < succ (succ x) +λ (x : ℕ), lt.step (zero_lt_succ x) diff --git a/tests/lean/nested2.lean b/tests/lean/nested2.lean new file mode 100644 index 000000000..7a9ea0369 --- /dev/null +++ b/tests/lean/nested2.lean @@ -0,0 +1,32 @@ +import data.nat data.list +open nat + +constant foo (a : nat) : a > 0 → nat + +definition bla (a : nat) := +foo + (succ (succ a)) + abstract lt.step abstract zero_lt_succ a end end + +print bla +print bla_1 +print bla_2 + +definition test (a : nat) := +foo + (succ (succ a)) + abstract [reducible] lt.step abstract [irreducible] zero_lt_succ a end end + +print test_1 +print test_2 + +constant voo {A : Type} (a b : A) : a ≠ b → bool + +set_option pp.universes true + +open list +definition tst {A : Type} (a : A) (l : list A) := +voo (a::l) [] abstract by contradiction end + +print tst_1 +print tst diff --git a/tests/lean/nested2.lean.expected.out b/tests/lean/nested2.lean.expected.out new file mode 100644 index 000000000..42b513514 --- /dev/null +++ b/tests/lean/nested2.lean.expected.out @@ -0,0 +1,15 @@ +definition bla : ℕ → ℕ +λ (a : ℕ), foo (succ (succ a)) (bla_2 a) +definition bla_1 : ∀ (x : ℕ), 0 < succ x +λ (x : ℕ), zero_lt_succ x +definition bla_2 : ∀ (x : ℕ), 0 < succ (succ x) +λ (x : ℕ), lt.step (bla_1 x) +definition test_1 [irreducible] : ∀ (x : ℕ), 0 < succ x +λ (x : ℕ), zero_lt_succ x +definition test_2 [reducible] : ∀ (x : ℕ), 0 < succ (succ x) +λ (x : ℕ), lt.step (test_1 x) +definition tst_1 : ∀ (x : Type.{l_1}) (x_1 : x) (x_2 : list.{l_1} x), + x_1 :: x_2 = nil.{l_1} → list.no_confusion_type.{0 l_1} false (x_1 :: x_2) nil.{l_1} +λ (x : Type.{l_1}) (x_1 : x) (x_2 : list.{l_1} x), list.no_confusion.{0 l_1} +definition tst : Π {A : Type.{l_1}}, A → list.{l_1} A → bool +λ (A : Type.{l_1}) (a : A) (l : list.{l_1} A), voo.{(max 1 l_1)} (a :: l) nil.{l_1} (tst_1.{l_1} A a l)