diff --git a/library/data/list/sort.lean b/library/data/list/sort.lean index 0bc41be3b6..7f63a5ea2e 100644 --- a/library/data/list/sort.lean +++ b/library/data/list/sort.lean @@ -29,8 +29,12 @@ include decA variable {R} variables (to : total R) (tr : transitive R) (rf : reflexive R) +section +include to tr rf lemma min_core_lemma : ∀ {b l} a, b ∈ l ∨ b = a → R (min_core R l a) b -:= using to tr rf, sorry +:= sorry +end + /- | b [] a h := or.elim h (suppose b ∈ [], absurd this !not_mem_nil) @@ -123,10 +127,12 @@ lemma min_mem : ∀ (l : list A) (h : l ≠ nil), min R l h ∈ l end -/ +section +include to tr rf lemma min_map (f : B → A) {l : list B} (h : l ≠ nil) : all l (λ b, (R (min R (map f l) (map_ne_nil_of_ne_nil _ h))) (f b)):= - using to tr rf, - sorry +sorry +end /- begin apply all_of_forall, diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index f655031627..ec0c741ba7 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -161,44 +161,6 @@ static expr parse_begin_end(parser & p, unsigned, expr const *, pos_info const & static expr parse_proof(parser & p); -static expr parse_using_expr(parser & p, pos_info const & using_pos) { - parser::local_scope scope(p); - buffer locals; - buffer new_locals; - while (!p.curr_is_token(get_comma_tk())) { - auto id_pos = p.pos(); - expr l = p.parse_id(); - if (!is_local(l)) - throw parser_error("invalid 'using' declaration, local expected", id_pos); - expr new_l; - binder_info bi = local_info(l); - if (p.is_local_variable_parameter(local_pp_name(l))) { - expr new_type = p.save_pos(mk_as_is(mlocal_type(l)), id_pos); - new_l = p.save_pos(mk_local(mlocal_name(l), local_pp_name(l), new_type, bi), id_pos); - } else { - new_l = p.save_pos(update_local(l, bi), id_pos); - } - p.add_local(new_l); - locals.push_back(l); - new_locals.push_back(new_l); - } - p.next(); // consume ',' - expr pr = p.parse_expr(); - unsigned i = locals.size(); - while (i > 0) { - --i; - expr l = locals[i]; - expr new_l = new_locals[i]; - pr = p.save_pos(Fun(new_l, pr), using_pos); - pr = p.save_pos(mk_app(pr, l), using_pos); - } - return pr; -} - -static expr parse_using(parser & p, unsigned, expr const *, pos_info const & pos) { - return parse_using_expr(p, pos); -} - static expr parse_proof(parser & p) { if (p.curr_is_token(get_from_tk())) { // parse: 'from' expr @@ -726,7 +688,6 @@ parse_table init_nud_table() { r = r.add({transition("@", mk_ext_action(parse_explicit_expr))}, x0); r = r.add({transition("@@", mk_ext_action(parse_partial_explicit_expr))}, x0); r = r.add({transition("begin", mk_ext_action_core(parse_begin_end))}, x0); - r = r.add({transition("using", mk_ext_action(parse_using))}, x0); r = r.add({transition("sorry", mk_ext_action(parse_sorry))}, x0); r = r.add({transition("match", mk_ext_action(parse_match))}, x0); r = r.add({transition("do", mk_ext_action(parse_do))}, x0); diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 4e0855b66b..252bb13a6e 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -95,7 +95,7 @@ void init_token_table(token_table & t) { {"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0}, {"Type", g_max_prec}, {"{|", g_max_prec}, {"|}", 0}, {"(:", g_max_prec}, {":)", 0}, {"⊢", 0}, {"⟨", g_max_prec}, {"⟩", 0}, {"^", 0}, {"↑", 0}, {"▸", 0}, - {"using", 0}, {"|", 0}, {"!", g_max_prec}, {"?", 0}, {"with", 0}, {"...", 0}, {",", 0}, + {"|", 0}, {"!", g_max_prec}, {"?", 0}, {"with", 0}, {"...", 0}, {",", 0}, {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {"as", 0}, {":=", 0}, {"--", 0}, {"#", 0}, {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"abstract", g_max_prec}, {"@@", g_max_prec}, {"@", g_max_prec}, diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp index 8f402a5158..3b548d54ea 100644 --- a/src/frontends/lean/tokens.cpp +++ b/src/frontends/lean/tokens.cpp @@ -78,7 +78,6 @@ static name const * g_in_tk = nullptr; static name const * g_at_tk = nullptr; static name const * g_assign_tk = nullptr; static name const * g_from_tk = nullptr; -static name const * g_using_tk = nullptr; static name const * g_then_tk = nullptr; static name const * g_else_tk = nullptr; static name const * g_by_tk = nullptr; @@ -222,7 +221,6 @@ void initialize_tokens() { g_at_tk = new name{"at"}; g_assign_tk = new name{":="}; g_from_tk = new name{"from"}; - g_using_tk = new name{"using"}; g_then_tk = new name{"then"}; g_else_tk = new name{"else"}; g_by_tk = new name{"by"}; @@ -367,7 +365,6 @@ void finalize_tokens() { delete g_at_tk; delete g_assign_tk; delete g_from_tk; - delete g_using_tk; delete g_then_tk; delete g_else_tk; delete g_by_tk; @@ -511,7 +508,6 @@ name const & get_in_tk() { return *g_in_tk; } name const & get_at_tk() { return *g_at_tk; } name const & get_assign_tk() { return *g_assign_tk; } name const & get_from_tk() { return *g_from_tk; } -name const & get_using_tk() { return *g_using_tk; } name const & get_then_tk() { return *g_then_tk; } name const & get_else_tk() { return *g_else_tk; } name const & get_by_tk() { return *g_by_tk; } diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h index 977d5aa501..b4ae5684f5 100644 --- a/src/frontends/lean/tokens.h +++ b/src/frontends/lean/tokens.h @@ -80,7 +80,6 @@ name const & get_in_tk(); name const & get_at_tk(); name const & get_assign_tk(); name const & get_from_tk(); -name const & get_using_tk(); name const & get_then_tk(); name const & get_else_tk(); name const & get_by_tk(); diff --git a/src/frontends/lean/tokens.txt b/src/frontends/lean/tokens.txt index c98a2ba38e..518d8e274a 100644 --- a/src/frontends/lean/tokens.txt +++ b/src/frontends/lean/tokens.txt @@ -73,7 +73,6 @@ in in at at assign := from from -using using then then else else by by