sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 18:34:06 +00:00
Code Issues Packages Projects Releases Wiki Activity

chore(frontends/lean): rename transient commands

Browse Source 
See issue #1432
This commit is contained in:
Leonardo de Moura
2017-03-09 17:24:26 -08:00
parent a00f2e49a7
commit 9d3c0497cb
490 changed files with 2204 additions and 2205 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
library/init/algebra/group.lean
View File

@@ -294,7 +294,7 @@ multiplicative_to_additive_pairs^.foldl (λ t ⟨src, tgt⟩, do
else t)
skip
run_command transport_multiplicative_to_additive
run_cmd transport_multiplicative_to_additive
instance add_semigroup_to_is_eq_associative [add_semigroup α] : is_associative α add :=
⟨add_assoc⟩

2
library/init/default.lean
View File

@@ -13,4 +13,4 @@ def debugger.attr : user_attribute :=
{ name := `breakpoint,
descr := "breakpoint for debugger" }
run_command attribute.register `debugger.attr
run_cmd attribute.register `debugger.attr

4
library/init/meta/smt/rsimp.lean
View File

@@ -45,8 +45,8 @@ do let t := ```(caching_user_attribute hinst_lemmas),
add_decl (declaration.defn attr_decl_name [] t v reducibility_hints.abbrev ff),
attribute.register attr_decl_name
run_command mk_name_set_attr `no_rsimp
run_command mk_hinst_lemma_attr_from_simp_attr `rsimp_attr `rsimp `simp `no_rsimp
run_cmd mk_name_set_attr `no_rsimp
run_cmd mk_hinst_lemma_attr_from_simp_attr `rsimp_attr `rsimp `simp `no_rsimp
/- The following lemmas are not needed by rsimp, and they actually hurt performance since they generate a lot of
instances. -/

4
library/init/meta/smt/smt_tactic.lean
View File

@@ -10,8 +10,8 @@ import init.meta.smt.ematch
universe u
run_command mk_simp_attr `pre_smt
run_command mk_hinst_lemma_attr_set `ematch [] [`ematch_lhs]
run_cmd mk_simp_attr `pre_smt
run_cmd mk_hinst_lemma_attr_set `ematch [] [`ematch_lhs]
/--
Configuration for the smt tactic preprocessor. The preprocessor

2
library/init/meta/tactic.lean
View File

@@ -979,7 +979,7 @@ end list
Remark: id_locked is used in the builtin implementation of tactic.change
-/
run_command do
run_cmd do
let l := level.param `l,
let Ty := expr.sort l,
type ← to_expr ``(Π (α : %%Ty), α → α),

2
library/tools/debugger/cli.lean
View File

@@ -232,4 +232,4 @@ meta def monitor : vm_monitor state :=
{ init := init_state, step := step_fn }
end debugger
run_command vm_monitor.register `debugger.monitor
run_cmd vm_monitor.register `debugger.monitor

2
library/tools/super/prover_state.lean
View File

@@ -381,7 +381,7 @@ meta def inference := derived_clause → prover unit
meta structure inf_decl := (prio : ℕ) (inf : inference)
meta def inf_attr : user_attribute :=
⟨ `super.inf, "inference for the super prover" ⟩
run_command attribute.register `super.inf_attr
run_cmd attribute.register `super.inf_attr
meta def seq_inferences : list inference → inference
| [] := λgiven, return ()

2
script/gen_constants_cpp.py
View File

@@ -91,7 +91,7 @@ def main(argv=None):
f.write("meta def script_check_id (n : name) : tactic unit :=\n");
f.write("do env ← get_env, (env^.get n >> return ()) <|> (guard $ env^.is_namespace n) <|> (attribute.get_instances n >> return ()) <|> fail (\"identifier '\" ++ to_string n ++ \"' is not a constant, namespace nor attribute\")\n");
for c in constants:
f.write("run_command script_check_id `%s\n" % c[1])
f.write("run_cmd script_check_id `%s\n" % c[1])
for c in constants:
cmd = ("cd .. && grep --silent --include=\"*.h\" --include=\"*.cpp\" --exclude=\".#*\" --exclude=\"constants.*\" -R \"get_%s_name\" *" % c[0])
if os.system(cmd) != 0:

13
src/emacs/lean-syntax.el
View File

@@ -9,20 +9,19 @@
(defconst lean-keywords1
'("import" "prelude" "protected" "private" "noncomputable" "definition" "meta" "renaming"
"hiding" "exposing" "parameter" "parameters" "begin" "conjecture" "constant" "constants"
"hypothesis" "lemma" "corollary" "variable" "variables" "premise" "premises" "theory"
"print" "theorem" "proposition" "example"
"hiding" "exposing" "parameter" "parameters" "begin" "constant" "constants"
"lemma" "variable" "variables" "#print" "theorem" "example"
"open" "as" "export" "override" "axiom" "axioms" "inductive" "with" "without"
"structure" "record" "universe" "universes"
"alias" "help" "precedence" "reserve" "declare_trace" "add_key_equivalence"
"structure" "universe" "universes"
"alias" "#help" "precedence" "reserve" "declare_trace" "add_key_equivalence"
"match" "infix" "infixl" "infixr" "notation" "postfix" "prefix" "instance"
"eval" "vm_eval" "check" "end" "this" "suppose"
"#eval" "#reduce" "#check" "end" "this" "suppose"
"using" "using_well_founded" "namespace" "section" "fields"
"attribute" "local" "set_option" "extends" "include" "omit" "classes" "class"
"instances" "coercions" "attributes" "raw" "replacing"
"calc" "have" "show" "suffices" "by" "in" "at" "do" "let" "forall" "Pi" "fun"
"exists" "if" "dif" "then" "else" "assume" "take" "obtain" "from" "aliases" "register_simp_ext"
"mutual" "def" "run_command")
"mutual" "def" "run_cmd")
"lean keywords ending with 'word' (not symbol)")
(defconst lean-keywords1-regexp
(eval `(rx word-start (or ,@lean-keywords1) word-end)))

36
src/frontends/lean/builtin_cmds.cpp
View File

@@ -179,14 +179,14 @@ environment check_cmd(parser & p) {
return p.env();
}
environment eval_cmd(parser & p) {
environment reduce_cmd(parser & p) {
bool whnf = false;
if (p.curr_is_token(get_whnf_tk())) {
p.next();
whnf = true;
}
expr e; level_param_names ls;
std::tie(e, ls) = parse_local_expr(p, "_eval");
std::tie(e, ls) = parse_local_expr(p, "_reduce");
expr r;
if (whnf) {
type_checker tc(p.env(), true, false);
@@ -197,7 +197,7 @@ environment eval_cmd(parser & p) {
r = normalize(tc, e, eta);
}
auto out = p.mk_message(p.cmd_pos(), INFORMATION);
out.set_caption("eval result") << r;
out.set_caption("reduce result") << r;
out.report();
return p.env();
}
@@ -420,11 +420,11 @@ static environment compile_expr(environment const & env, name const & n, level_p
return vm_compile(new_env, new_env.get(n));
}
static void vm_eval_core(vm_state & s, name const & main, optional<vm_obj> const & initial_state) {
static void eval_core(vm_state & s, name const & main, optional<vm_obj> const & initial_state) {
if (initial_state) s.push(*initial_state); // push initial_state for IO/tactic monad.
vm_decl d = *s.get_decl(main);
if (!initial_state && d.get_arity() > 0)
throw exception("vm_eval result is a function");
throw exception("eval result is a function");
s.invoke_fn(main);
if (initial_state) {
if (d.get_arity() == 0) {
@@ -435,12 +435,12 @@ static void vm_eval_core(vm_state & s, name const & main, optional<vm_obj> const
}
}
static environment vm_eval_cmd(parser & p) {
static environment eval_cmd(parser & p) {
auto pos = p.pos();
expr e; level_param_names ls;
std::tie(e, ls) = parse_local_expr(p, "_eval");
if (has_metavar(e))
throw parser_error("invalid vm_eval command, expression contains metavariables", pos);
throw parser_error("invalid eval command, expression contains metavariables", pos);
type_context tc(p.env(), transparency_mode::All);
expr type0 = tc.infer(e);
expr type = tc.whnf(type0);
@@ -465,14 +465,14 @@ static environment vm_eval_cmd(parser & p) {
optional<vm_obj> initial_state;
if (is_io) initial_state = mk_vm_simple(0);
auto out = p.mk_message(p.cmd_pos(), INFORMATION);
out.set_caption("vm_eval result");
out.set_caption("eval result");
vm_state::profiler prof(s, p.get_options());
// TODO(gabriel): capture output
if (p.profiling()) {
timeit timer(out.get_text_stream().get_stream(), "vm_eval time");
vm_eval_core(s, main, initial_state);
timeit timer(out.get_text_stream().get_stream(), "eval time");
eval_core(s, main, initial_state);
} else {
vm_eval_core(s, main, initial_state);
eval_core(s, main, initial_state);
}
if (is_io) {
// do not print anything
@@ -549,20 +549,20 @@ void init_cmd_table(cmd_table & r) {
open_cmd));
add_cmd(r, cmd_info("export", "create aliases for declarations", export_cmd));
add_cmd(r, cmd_info("set_option", "set configuration option", set_option_cmd));
add_cmd(r, cmd_info("exit", "exit", exit_cmd));
add_cmd(r, cmd_info("print", "print a string", print_cmd));
add_cmd(r, cmd_info("#exit", "exit", exit_cmd));
add_cmd(r, cmd_info("#print", "print a string or information about an indentifier", print_cmd));
add_cmd(r, cmd_info("section", "open a new section", section_cmd));
add_cmd(r, cmd_info("namespace", "open a new namespace", namespace_cmd));
add_cmd(r, cmd_info("end", "close the current namespace/section", end_scoped_cmd));
add_cmd(r, cmd_info("check", "type check given expression, and display its type", check_cmd));
add_cmd(r, cmd_info("eval", "evaluate given expression", eval_cmd));
add_cmd(r, cmd_info("vm_eval", "VM evaluation", vm_eval_cmd));
add_cmd(r, cmd_info("#check", "type check given expression, and display its type", check_cmd));
add_cmd(r, cmd_info("#reduce", "reduce given expression", reduce_cmd));
add_cmd(r, cmd_info("#eval", "evaluate given expression using VM", eval_cmd));
add_cmd(r, cmd_info("local", "define local attributes or notation", local_cmd));
add_cmd(r, cmd_info("help", "brief description of available commands and options", help_cmd));
add_cmd(r, cmd_info("#help", "brief description of available commands and options", help_cmd));
add_cmd(r, cmd_info("init_quotient", "initialize quotient type computational rules", init_quotient_cmd));
add_cmd(r, cmd_info("declare_trace", "declare a new trace class (for debugging Lean tactics)", declare_trace_cmd));
add_cmd(r, cmd_info("add_key_equivalence", "register that to symbols are equivalence for key-matching", add_key_equivalence_cmd));
add_cmd(r, cmd_info("run_command", "execute an user defined command at top-level", run_command_cmd));
add_cmd(r, cmd_info("run_cmd", "execute an user defined command at top-level", run_command_cmd));
add_cmd(r, cmd_info("import", "import module(s)", import_cmd));
add_cmd(r, cmd_info("#unify", "(for debugging purposes)", unify_cmd));
add_cmd(r, cmd_info("#compile", "(for debugging purposes)", compile_cmd));

32
src/frontends/lean/print_cmd.cpp
View File

@@ -80,7 +80,7 @@ struct print_axioms_deps {
static void print_axioms(parser & p, message_builder & out) {
if (p.curr_is_identifier()) {
name c = p.check_constant_next("invalid 'print axioms', constant expected");
name c = p.check_constant_next("invalid '#print axioms', constant expected");
auto env = p.env();
type_context tc(env, p.get_options());
auto new_out = io_state_stream(env, p.ios(), tc, out.get_text_stream().get_channel());
@@ -100,7 +100,7 @@ static void print_axioms(parser & p, message_builder & out) {
}
static void print_prefix(parser & p, message_builder & out) {
name prefix = p.check_id_next("invalid 'print prefix' command, identifier expected");
name prefix = p.check_id_next("invalid '#print prefix' command, identifier expected");
buffer<declaration> to_print;
p.env().for_each_declaration([&](declaration const & d) {
if (is_prefix_of(prefix, d.get_name())) {
@@ -118,7 +118,7 @@ static void print_prefix(parser & p, message_builder & out) {
static void print_fields(parser const & p, message_builder & out, name const & S, pos_info const & pos) {
environment const & env = p.env();
if (!is_structure(env, S))
throw parser_error(sstream() << "invalid 'print fields' command, '" << S << "' is not a structure", pos);
throw parser_error(sstream() << "invalid '#print fields' command, '" << S << "' is not a structure", pos);
buffer<name> field_names;
get_structure_fields(env, S, field_names);
for (name const & field_name : field_names) {
@@ -224,7 +224,7 @@ static name to_user_name(environment const & env, name const & n) {
static void print_definition(environment const & env, message_builder & out, name const & n, pos_info const & pos) {
declaration d = env.get(n);
if (!d.is_definition())
throw parser_error(sstream() << "invalid 'print definition', '" << to_user_name(env, n) << "' is not a definition", pos);
throw parser_error(sstream() << "invalid '#print definition', '" << to_user_name(env, n) << "' is not a definition", pos);
options opts = out.get_text_stream().get_options();
opts = opts.update_if_undef(get_pp_beta_name(), false);
out.get_text_stream().update_options(opts) << d.get_value() << endl;
@@ -282,12 +282,12 @@ static void print_inductive(parser const & p, message_builder & out, name const
}
}
} else {
throw parser_error(sstream() << "invalid 'print inductive', '" << n << "' is not an inductive declaration", pos);
throw parser_error(sstream() << "invalid '#print inductive', '" << n << "' is not an inductive declaration", pos);
}
}
static void print_recursor_info(parser & p, message_builder & out) {
name c = p.check_constant_next("invalid 'print [recursor]', constant expected");
name c = p.check_constant_next("invalid '#print [recursor]', constant expected");
recursor_info info = get_recursor_info(p.env(), c);
out << "recursor information\n"
<< " num. parameters: " << info.get_num_params() << "\n"
@@ -461,13 +461,13 @@ static void print_unification_hints(parser & p, message_builder & out) {
}
static void print_simp_rules(parser & p, message_builder & out) {
name attr = p.check_id_next("invalid 'print [simp]' command, identifier expected");
name attr = p.check_id_next("invalid '#print [simp]' command, identifier expected");
simp_lemmas slss = get_simp_lemmas(p.env(), transparency_mode::Reducible, attr);
out << slss.pp_simp(out.get_formatter());
}
static void print_congr_rules(parser & p, message_builder & out) {
name attr = p.check_id_next("invalid 'print [congr]' command, identifier expected");
name attr = p.check_id_next("invalid '#print [congr]' command, identifier expected");
simp_lemmas slss = get_simp_lemmas(p.env(), transparency_mode::Reducible, attr);
out << slss.pp_congr(out.get_formatter());
}
@@ -532,8 +532,8 @@ environment print_cmd(parser & p) {
} else if (p.curr_is_token_or_id(get_definition_tk())) {
p.next();
auto pos = p.pos();
name id = p.check_id_next("invalid 'print definition', constant expected");
list<name> cs = p.to_constants(id, "invalid 'print definition', constant expected", pos);
name id = p.check_id_next("invalid '#print definition', constant expected");
list<name> cs = p.to_constants(id, "invalid '#print definition', constant expected", pos);
bool first = true;
for (name const & c : cs) {
if (first)
@@ -548,12 +548,12 @@ environment print_cmd(parser & p) {
print_constant(p, out, "definition", d);
print_definition(env, out, c, pos);
} else {
throw parser_error(sstream() << "invalid 'print definition', '" << to_user_name(p.env(), c) << "' is not a definition", pos);
throw parser_error(sstream() << "invalid '#print definition', '" << to_user_name(p.env(), c) << "' is not a definition", pos);
}
}
} else if (p.curr_is_token_or_id(get_instances_tk())) {
p.next();
name c = p.check_constant_next("invalid 'print instances', constant expected");
name c = p.check_constant_next("invalid '#print instances', constant expected");
for (name const & i : get_class_instances(env, c)) {
out << i << " : " << env.get(i).get_type() << endl;
}
@@ -587,7 +587,7 @@ environment print_cmd(parser & p) {
} else if (p.curr_is_token_or_id(get_fields_tk())) {
p.next();
auto pos = p.pos();
name S = p.check_constant_next("invalid 'print fields' command, constant expected");
name S = p.check_constant_next("invalid '#print fields' command, constant expected");
print_fields(p, out, S, pos);
} else if (p.curr_is_token_or_id(get_notation_tk())) {
p.next();
@@ -595,13 +595,13 @@ environment print_cmd(parser & p) {
} else if (p.curr_is_token_or_id(get_inductive_tk())) {
p.next();
auto pos = p.pos();
name c = p.check_constant_next("invalid 'print inductive', constant expected");
name c = p.check_constant_next("invalid '#print inductive', constant expected");
print_inductive(p, out, c, pos);
} else if (p.curr_is_token(get_lbracket_tk())) {
p.next();
auto pos = p.pos();
auto name = p.check_id_next("invalid attribute declaration, identifier expected");
p.check_token_next(get_rbracket_tk(), "invalid 'print [<attr>]', ']' expected");
p.check_token_next(get_rbracket_tk(), "invalid '#print [<attr>]', ']' expected");
if (name == "recursor") {
print_recursor_info(p, out);
@@ -619,7 +619,7 @@ environment print_cmd(parser & p) {
}
} else if (print_polymorphic(p, out)) {
} else {
throw parser_error("invalid print command", p.pos());
throw parser_error("invalid '#print' command", p.pos());
}
out.report();
return p.env();

9
src/frontends/lean/token_table.cpp
View File

@@ -104,13 +104,14 @@ void init_token_table(token_table & t) {
{"theorem", "axiom", "axioms", "variable", "protected", "private",
"definition", "meta", "mutual", "example", "noncomputable",
"variables", "parameter", "parameters", "constant", "constants",
"check", "eval", "vm_eval", "using_well_founded", "[whnf]",
"print", "end", "namespace", "section", "prelude", "help",
"using_well_founded", "[whnf]",
"end", "namespace", "section", "prelude",
"import", "inductive", "structure", "class", "universe", "universes", "local",
"precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation",
"exit", "set_option", "open", "export", "@[",
"set_option", "open", "export", "@[",
"attribute", "instance", "include", "omit", "init_quotient",
"declare_trace", "run_command", "add_key_equivalence",
"declare_trace", "add_key_equivalence",
"run_cmd", "#check", "#reduce", "#eval", "#print", "#help", "#exit",
"#compile", "#unify", nullptr};
pair<char const *, char const *> aliases[] =

2
tests/lean/1292.lean
View File

@@ -1,7 +1,7 @@
def fn (n : nat) : nat :=
match n with
exit
#exit
theorem thm : true := begin end

6
tests/lean/1299.lean
View File

@@ -7,8 +7,8 @@ add_decl (declaration.ax `new_ax [] prt),
l ← to_expr `(new_ax),
apply l
check d1
print d1
#check d1
#print d1
theorem d2 : true = true := by do
trace (("a", "a")),
@@ -17,4 +17,4 @@ add_decl (declaration.ax `new_ax2 [] prt),
l ← to_expr `(new_ax2),
apply l
print d2
#print d2

4
tests/lean/1334a.lean
View File

@@ -8,5 +8,5 @@ def fn : nlist → nlist
| (mk l) := mk []
| _ := atom
check fn.equations._eqn_1
check fn.equations._eqn_2
#check fn.equations._eqn_1
#check fn.equations._eqn_2

12
tests/lean/1334b.lean
View File

@@ -7,17 +7,17 @@ def var_of : term → option nat
| (term.var n) := some n
| _ := none
check var_of.equations._eqn_1
check var_of.equations._eqn_2
check var_of.equations._eqn_3
#check var_of.equations._eqn_1
#check var_of.equations._eqn_2
#check var_of.equations._eqn_3
def list_of : term → list term
| (term.app ts) := ts
| _ := []
check list_of.equations._eqn_1
check list_of.equations._eqn_2
check list_of.equations._eqn_3
#check list_of.equations._eqn_1
#check list_of.equations._eqn_2
#check list_of.equations._eqn_3
example (a : nat) (ls : list term) : term.var a = term.app ls → false :=
by contradiction

8
tests/lean/584a.lean
View File

@@ -3,17 +3,17 @@ variables (A : Type u) [H : inhabited A] (x : A)
include H
definition foo := x
check foo -- A and x are explicit
#check foo -- A and x are explicit
variables {A x}
definition foo' := x
check @foo' -- A is explicit, x is implicit
#check @foo' -- A is explicit, x is implicit
open nat
check foo nat 10
#check foo nat 10
definition test : foo' = (10:nat) := rfl
set_option pp.implicit true
print test
#print test

8
tests/lean/584b.lean
View File

@@ -7,21 +7,21 @@ section
definition tst₁ := a
check @tst₁
#check @tst₁
variable {A}
definition tst₂ := a
check @tst₂ -- A is implicit
#check @tst₂ -- A is implicit
lemma symm₂ : b = a := eq.symm H
check @symm₂
#check @symm₂
end
variable (a : A)
definition tst₃ := a
check @tst₃ -- A is explicit again
#check @tst₃ -- A is explicit again
end

10
tests/lean/584c.lean
View File

@@ -22,8 +22,8 @@ section
definition tst₃ := a
end
check @tst₁
check @tst₂ -- A is implicit
check @symm₂
check @tst₃ -- A is explicit again
check @foo
#check @tst₁
#check @tst₂ -- A is implicit
#check @symm₂
#check @tst₃ -- A is explicit again
#check @foo

10
tests/lean/634.lean
View File

@@ -5,13 +5,13 @@ section
definition A {n : ℕ} : Type := X
variable {n : ℕ}
set_option pp.implicit true
check @A n
#check @A n
set_option pp.full_names true
check @foo.A n
check @A n
#check @foo.A n
#check @A n
set_option pp.full_names false
check @foo.A n
check @A n
#check @foo.A n
#check @A n
end
end foo

46
tests/lean/634b.lean
View File

@@ -5,37 +5,37 @@ section
definition A {n : ℕ} : Type := X
definition B : Type := X
variable {n : ℕ}
check @A n
check foo.A
check foo.A
check @foo.A 10
check @foo.A n
check @foo.A n
check @foo.A n
#check @A n
#check foo.A
#check foo.A
#check @foo.A 10
#check @foo.A n
#check @foo.A n
#check @foo.A n
set_option pp.full_names true
check A
check foo.A
check @foo.A 10
check @foo.A n
check @foo.A n
#check A
#check foo.A
#check @foo.A 10
#check @foo.A n
#check @foo.A n
set_option pp.full_names false
set_option pp.implicit true
check @A n
check @foo.A 10
check @foo.A n
#check @A n
#check @foo.A 10
#check @foo.A n
set_option pp.full_names true
check @foo.A n
check @A n
#check @foo.A n
#check @A n
set_option pp.full_names false
check @foo.A n
check @foo.A n
check @foo.A n
check @foo.A n
check @foo.A n
check @A n
#check @foo.A n
#check @foo.A n
#check @foo.A n
#check @foo.A n
#check @foo.A n
#check @A n
end
end foo

44
tests/lean/634c.lean
View File

@@ -4,35 +4,35 @@ section
definition A {n : ℕ} : Type := X
definition B : Type := X
variable {n : ℕ}
check @A n
check _root_.A nat
check _root_.A (X × B)
check @_root_.A (X × B) 10
check @_root_.A (_root_.B (@_root_.A X n)) n
check @_root_.A (@_root_.B (@_root_.A nat n)) n
#check @A n
#check _root_.A nat
#check _root_.A (X × B)
#check @_root_.A (X × B) 10
#check @_root_.A (_root_.B (@_root_.A X n)) n
#check @_root_.A (@_root_.B (@_root_.A nat n)) n
set_option pp.full_names true
check A
check _root_.A nat
check @_root_.A (X × B) 10
check @_root_.A (@_root_.B (@_root_.A X n)) n
check @_root_.A (@_root_.B (@_root_.A nat n)) n
#check A
#check _root_.A nat
#check @_root_.A (X × B) 10
#check @_root_.A (@_root_.B (@_root_.A X n)) n
#check @_root_.A (@_root_.B (@_root_.A nat n)) n
set_option pp.full_names false
set_option pp.implicit true
check @A n
check @_root_.A nat 10
check @_root_.A X n
#check @A n
#check @_root_.A nat 10
#check @_root_.A X n
set_option pp.full_names true
check @_root_.A X n
check @_root_.A B n
#check @_root_.A X n
#check @_root_.A B n
set_option pp.full_names false
check @_root_.A X n
check @_root_.A B n
check @_root_.A (@_root_.B (@A n)) n
check @_root_.A (@_root_.B (@_root_.A X n)) n
check @_root_.A (@_root_.B (@_root_.A nat n)) n
check @A n
#check @_root_.A X n
#check @_root_.A B n
#check @_root_.A (@_root_.B (@A n)) n
#check @_root_.A (@_root_.B (@_root_.A X n)) n
#check @_root_.A (@_root_.B (@_root_.A nat n)) n
#check @A n
end

20
tests/lean/634d.lean
View File

@@ -1,23 +1,23 @@
section
universe l
definition A {n : ℕ} (t : Sort l) := t
check A
check _root_.A.{1}
#check A
#check _root_.A.{1}
set_option pp.universes true
check A
check _root_.A.{1}
#check A
#check _root_.A.{1}
end
section
universe l
parameters {B : Sort l}
definition P {n : ℕ} (b : B) := b
check P
check @_root_.P.{1} nat
#check P
#check @_root_.P.{1} nat
set_option pp.universes true
check P
check _root_.P.{1}
#check P
#check _root_.P.{1}
set_option pp.implicit true
check @P 2
check @_root_.P.{1} nat
#check @P 2
#check @_root_.P.{1} nat
end

12
tests/lean/652.lean
View File

@@ -17,9 +17,9 @@ section
definition R6 := R
end
check @R
check @R2
check @R3
check @R4
check @R5
check @R6
#check @R
#check @R2
#check @R3
#check @R4
#check @R5
#check @R6

2
tests/lean/671.lean
View File

@@ -1 +1 @@
print nat.add
#print nat.add

12
tests/lean/712.lean
View File

@@ -4,21 +4,21 @@ reserve notation `[` a `][` b:10 `]`
section
local infix `~~~` := eq
print notation ~~~
#print notation ~~~
local infix `~~~`:50 := eq
print notation ~~~
#print notation ~~~
local infix `~~~`:100 := eq
infix `~~~`:100 := eq -- FAIL
print notation ~~~
#print notation ~~~
local notation `[` a `][`:10 b:20 `]` := a = b
print notation ][
#print notation ][
end
notation `[` a `][`:10 b:20 `]` := a = b -- FAIL
@@ -26,5 +26,5 @@ notation `[` a `][`:10 b:20 `]` := a = b -- FAIL
notation `[` a `][` b `]` := a = b
infix `~~~` := eq
print notation ~~~
print notation ][
#print notation ~~~
#print notation ][

10
tests/lean/alias.lean
View File

@@ -13,12 +13,12 @@ end N2
open N2
open N1
constants a b : N1.num
print raw foo a b
#print raw foo a b
open N2
print raw foo a b
#print raw foo a b
open N1
print raw foo a b
#print raw foo a b
open N1
print raw foo a b
#print raw foo a b
open N2
print raw foo a b
#print raw foo a b

2
tests/lean/alias2.lean
View File

@@ -7,5 +7,5 @@ open foo
namespace bla
definition t := false
check foo.t -- <<< must print foo.t : Prop instead of t : Prop
#check foo.t -- <<< must print foo.t : Prop instead of t : Prop
end bla

24
tests/lean/anc1.lean
View File

@@ -1,48 +1,48 @@
check (⟨1, 2⟩ : nat × nat)
#check (⟨1, 2⟩ : nat × nat)
check (⟨trivial, trivial⟩ : true ∧ true)
#check (⟨trivial, trivial⟩ : true ∧ true)
example : true := sorry
check (⟨1, sorry⟩ : Σ' x : nat, x > 0)
#check (⟨1, sorry⟩ : Σ' x : nat, x > 0)
open tactic
check show true, from ⟨⟩
#check show true, from ⟨⟩
check (⟨1, by intro1 >> contradiction⟩ : ∃ x : nat, 1 ≠ 0)
#check (⟨1, by intro1 >> contradiction⟩ : ∃ x : nat, 1 ≠ 0)
universe variables u v
check λ (A B C : Prop),
#check λ (A B C : Prop),
assume (Ha : A) (Hb : B) (Hc : C),
show B ∧ A, from
⟨Hb, Ha⟩
check λ (A B C : Prop),
#check λ (A B C : Prop),
assume (Ha : A) (Hb : B) (Hc : C),
show B ∧ A ∧ C ∧ A, from
⟨Hb, ⟨Ha, ⟨Hc, Ha⟩⟩⟩
check λ (A B C : Prop),
#check λ (A B C : Prop),
assume (Ha : A) (Hb : B) (Hc : C),
show B ∧ A ∧ C ∧ A, from
⟨Hb, Ha, Hc, Ha⟩
check λ (A B C : Prop),
#check λ (A B C : Prop),
assume (Ha : A) (Hb : B) (Hc : C),
show ((B ∧ true) ∧ A) ∧ (C ∧ A), from
⟨⟨⟨Hb, ⟨⟩⟩, Ha⟩, ⟨Hc, Ha⟩⟩
check λ (A : Type u) (P : A → Prop) (Q : A → Prop),
#check λ (A : Type u) (P : A → Prop) (Q : A → Prop),
take (a : A), assume (H1 : P a) (H2 : Q a),
show ∃ x, P x ∧ Q x, from
⟨a, ⟨H1, H2⟩⟩
check λ (A : Type u) (P : A → Prop) (Q : A → Prop),
#check λ (A : Type u) (P : A → Prop) (Q : A → Prop),
take (a : A) (b : A), assume (H1 : P a) (H2 : Q b),
show ∃ x y, P x ∧ Q y, from
⟨a, ⟨b, ⟨H1, H2⟩⟩⟩
check λ (A : Type u) (P : A → Prop) (Q : A → Prop),
#check λ (A : Type u) (P : A → Prop) (Q : A → Prop),
take (a : A) (b : A), assume (H1 : P a) (H2 : Q b),
show ∃ x y, P x ∧ Q y, from
⟨a, b, H1, H2⟩

2
tests/lean/assert_tac3.lean
View File

@@ -11,7 +11,7 @@ by do
exact a,
return ()
print tst2
#print tst2
definition tst3 (a b : nat) : a = a :=
by do

2
tests/lean/attribute_bug1.lean
View File

@@ -13,7 +13,7 @@ by simp -- Succeeded as expected
local attribute [-simp] fdef
print fdef -- we don't get the [simp] attribute when printing fdef
#print fdef -- we don't get the [simp] attribute when printing fdef
example (n : nat) : f n = n + 1 :=
by simp -- Failed as expected, since we removed [simp] attribute

6
tests/lean/bad_print.lean
View File

@@ -1,7 +1,7 @@
constant boo : nat
print definition boo
#print definition boo
print 2
#print 2
print fields nat
#print fields nat

6
tests/lean/bad_print.lean.expected.out
View File

@@ -1,3 +1,3 @@
bad_print.lean:3:17: error: invalid 'print definition', 'boo' is not a definition
bad_print.lean:5:6: error: invalid print command
bad_print.lean:7:13: error: invalid 'print fields' command, 'nat' is not a structure
bad_print.lean:3:18: error: invalid '#print definition', 'boo' is not a definition
bad_print.lean:5:7: error: invalid '#print' command
bad_print.lean:7:14: error: invalid '#print fields' command, 'nat' is not a structure

2
tests/lean/bug1.lean
View File

@@ -20,4 +20,4 @@ theorem and_intro3 (p q : bool) (H1 : p) (H2 : q) : q ∧ p
theorem and_intro4 (p q : bool) (H1 : p) (H2 : q) : p ∧ q
:= fun (c : bool) (H : p -> q -> c), H H1 H2
check and_intro4
#check and_intro4

6
tests/lean/by_contradiction.lean
View File

@@ -7,7 +7,7 @@ by do
trace_state,
contradiction
print "-------"
#print "-------"
example (a b : nat) : ¬¬ a = b → a = b :=
by do
@@ -16,7 +16,7 @@ by do
trace_state,
contradiction
print "-------"
#print "-------"
example (p q : Prop) : ¬¬ p → p :=
by do
@@ -24,7 +24,7 @@ by do
by_contradiction `H, -- should fail
trace_state
print "-------"
#print "-------"
local attribute [instance] classical.prop_decidable -- Now all propositions are decidable

10
tests/lean/caching_user_attribute.lean
View File

@@ -3,29 +3,29 @@ meta def foo_attr : caching_user_attribute string :=
mk_cache := λ ns, return $ list.join ∘ list.map (list.append "\n" ∘ to_string) $ ns,
dependencies := [] }
run_command attribute.register `foo_attr
run_cmd attribute.register `foo_attr
attribute [foo] eq.refl eq.mp
set_option trace.user_attributes_cache true
run_command do
run_cmd do
s : string ← caching_user_attribute.get_cache foo_attr,
tactic.trace s
run_command do
run_cmd do
s : string ← caching_user_attribute.get_cache foo_attr,
tactic.trace s
attribute [foo] eq.mpr
local attribute [-foo] eq.mp
run_command do
run_cmd do
s : string ← caching_user_attribute.get_cache foo_attr,
tactic.trace s
attribute [reducible] eq.mp -- should not affect [foo] cache
run_command do
run_cmd do
s : string ← caching_user_attribute.get_cache foo_attr,
tactic.trace s

6
tests/lean/calc1.lean
View File

@@ -23,7 +23,7 @@ axiom H1 : a = b
axiom H2 : b ≤ c
axiom H3 : c ≤ d
axiom H4 : d = e
check calc a = b : H1
#check calc a = b : H1
... ≤ c : H2
... ≤ d : H3
... = e : H4
@@ -34,10 +34,10 @@ axiom lt_trans (a b c : A) (H1 : a < b) (H2 : b < c) : a < c
axiom le_lt_trans (a b c : A) (H1 : a ≤ b) (H2 : b < c) : a < c
axiom lt_le_trans (a b c : A) (H1 : a < b) (H2 : b ≤ c) : a < c
axiom H5 : c < d
-- check calc b ≤ c : H2
-- #check calc b ≤ c : H2
-- ... < d : H5 -- Error le_lt_trans was not registered yet
attribute [trans] le_lt_trans
check calc b ≤ c : H2
#check calc b ≤ c : H2
... < d : H5
constant le2 : A → A → bool

2
tests/lean/cases_induction_fresh.lean
View File

@@ -7,7 +7,7 @@ begin
constructor; assumption
end
print "------------"
#print "------------"
example (p q r s: Prop): p ∧ q → r ∧ s → s ∧ q :=
begin

16
tests/lean/char_lits.lean
View File

@@ -1,11 +1,11 @@
import system.io
open io
check #"a"
#check #"a"
vm_eval #"a"
vm_eval #"\n"
vm_eval #"\\"
vm_eval put_str (list.cons #"\\" "aaa")
vm_eval put_str [#"\n"]
vm_eval put_str [#"\n"]
vm_eval put_str (list.cons #"\'" "aaa")
#eval #"a"
#eval #"\n"
#eval #"\\"
#eval put_str (list.cons #"\\" "aaa")
#eval put_str [#"\n"]
#eval put_str [#"\n"]
#eval put_str (list.cons #"\'" "aaa")

8
tests/lean/check.lean
View File

@@ -1,6 +1,6 @@
--
check and.intro
check or.elim
check eq
check eq.rec
#check and.intro
#check or.elim
#check eq
#check eq.rec

2
tests/lean/check2.lean
View File

@@ -1,3 +1,3 @@
--
check eq.rec_on
#check eq.rec_on

6
tests/lean/choice_expl.lean
View File

@@ -10,6 +10,6 @@ end N2
open N1 N2
constant N : Type.{1}
constants a b : N
check @N1.pr
check @N2.pr N a b
check pr a b
#check @N1.pr
#check @N2.pr N a b
#check pr a b

4
tests/lean/choice_expl.lean.expected.out
View File

@@ -1,8 +1,8 @@
pr : Π {A : Type u_1}, A → A → A
pr a b : N
choice_expl.lean:15:6: error: ambiguous overload, possible interpretations
choice_expl.lean:15:7: error: ambiguous overload, possible interpretations
N2.pr a b
N1.pr a b
Additional information:
choice_expl.lean:15:6: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because expected type was not available
choice_expl.lean:15:7: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because expected type was not available
sorry : ?M_1

24
tests/lean/coe1.lean
View File

@@ -1,5 +1,5 @@
namespace hidden
check if tt then "a" else "b"
#check if tt then "a" else "b"
/- Remark: in the standard library nat_to_int and int_to_real are has_lift instances
instead of has_coe. -/
constant int : Type
@@ -13,29 +13,29 @@ constants n m : nat
constants i j : int
constants x y : real
check sine x
check sine n
check sine i
#check sine x
#check sine n
#check sine i
constant int_has_add : has_add int
constant real_has_add : has_add real
attribute [instance] int_has_add real_has_add
check x + i
#check x + i
/- The following one does not work because the implicit argument ?A of add is bound to int
when x is processed. -/
check i + x -- FAIL
#check i + x -- FAIL
/- The workaround is to use the explicit lift -/
check ↑i + x
#check ↑i + x
check x + n
#check x + n
check n + x -- FAIL
#check n + x -- FAIL
check ↑n + x
#check ↑n + x
check (i:real) + x
check (n:real) + x
#check (i:real) + x
#check (n:real) + x
end hidden

4
tests/lean/coe1.lean.expected.out
View File

@@ -3,7 +3,7 @@ sine x : real
sine ↑n : real
sine ↑i : real
x + ↑i : real
coe1.lean:28:8: error: type mismatch at application
coe1.lean:28:9: error: type mismatch at application
i + x
term
x
@@ -14,7 +14,7 @@ but is expected to have type
sorry : ?M_1
↑i + x : real
x + ↑n : real
coe1.lean:35:8: error: type mismatch at application
coe1.lean:35:9: error: type mismatch at application
n + x
term
x

20
tests/lean/coe2.lean
View File

@@ -1,6 +1,6 @@
namespace hidden
set_option pp.coercions false
check if tt then "a" else "b"
#check if tt then "a" else "b"
/- Remark: in the standard library nat_to_int and int_to_real are has_lift instances
instead of has_coe. -/
@@ -15,26 +15,26 @@ constants n m : nat
constants i j : int
constants x y : real
check sine x
check sine n
check sine i
#check sine x
#check sine n
#check sine i
constant int_has_add : has_add int
constant real_has_add : has_add real
attribute [instance] int_has_add real_has_add
check x + i
#check x + i
/- The following one does not work because the implicit argument ?A of add is bound to int
when x is processed. -/
check i + x -- FAIL
#check i + x -- FAIL
/- The workaround is to use the explicit lift -/
check ↑i + x
#check ↑i + x
check x + n
#check x + n
check n + x -- FAIL
#check n + x -- FAIL
check ↑n + x
#check ↑n + x
end hidden

4
tests/lean/coe2.lean.expected.out
View File

@@ -3,7 +3,7 @@ sine x : real
sine n : real
sine i : real
x + i : real
coe2.lean:30:8: error: type mismatch at application
coe2.lean:30:9: error: type mismatch at application
i + x
term
x
@@ -14,7 +14,7 @@ but is expected to have type
sorry : ?M_1
i + x : real
x + n : real
coe2.lean:37:8: error: type mismatch at application
coe2.lean:37:9: error: type mismatch at application
n + x
term
x

4
tests/lean/coe3.lean
View File

@@ -11,6 +11,6 @@ constant a : A
constant f : C → C
constant g : D → D
check f a
#check f a
check g a
#check g a

8
tests/lean/coe4.lean
View File

@@ -10,16 +10,16 @@ definition coe_functor_to_fn (A : Type u) : has_coe_to_fun (Functor A) :=
constant f : Functor nat
check f 0 1
#check f 0 1
set_option pp.coercions false
check f 0 1
#check f 0 1
set_option pp.coercions true
check f 0 1
#check f 0 1
set_option pp.all true
check f 0 1
#check f 0 1

10
tests/lean/coe5.lean
View File

@@ -7,17 +7,17 @@ meta def expr_to_app : has_coe_to_fun expr :=
meta constants f a b : expr
check f a
#check f a
check f a b
#check f a b
check f a b a
#check f a b a
set_option pp.coercions false
check f a b a
#check f a b a
set_option pp.all true
set_option pp.coercions true
check f a b
#check f a b

2
tests/lean/coe6.lean
View File

@@ -9,4 +9,4 @@ definition Group_to_Type : has_coe_to_sort Group :=
constant g : Group.{1}
set_option pp.binder_types true
check λ a b : g, Group.mul g a b
#check λ a b : g, Group.mul g a b

8
tests/lean/concrete_instance.lean
View File

@@ -2,11 +2,11 @@ variables a b : nat
set_option pp.all true
check a * b
check a + b
#check a * b
#check a + b
-- instance : semigroup nat := sorry
-- instance : add_semigroup nat := sorry
check a * b
check a + b
#check a * b
#check a + b

4
tests/lean/const.lean
View File

@@ -12,6 +12,6 @@ section
variable A : Type u
variable S : inhabited A
variable B : @bla A S
check B
check @foo A S
#check B
#check @foo A S
end

4
tests/lean/ctxopt.lean
View File

@@ -3,7 +3,7 @@
section
set_option pp.implicit true
check id true
#check id true
end
check id true
#check id true

26
tests/lean/curly_notation.lean
View File

@@ -1,26 +1,26 @@
check ({1, 2, 3} : set nat)
check ({1} : set nat)
check ({} : set nat)
#check ({1, 2, 3} : set nat)
#check ({1} : set nat)
#check ({} : set nat)
definition s1 : set nat := {1, 2+3, 3, 4}
print s1
#print s1
definition s2 : set char := {#"a", #"b", #"c"}
print s2
#print s2
definition s3 : set string := {"hello", "world"}
print s3
#print s3
check { a ∈ s1 | a > 1 }
check { a in s1 | a > 1 }
#check { a ∈ s1 | a > 1 }
#check { a in s1 | a > 1 }
set_option pp.unicode false
check { a ∈ s1 | a > 2 }
#check { a ∈ s1 | a > 2 }
definition a := 10
check ({a, a} : set nat)
check ({a, 1, a} : set nat)
check ({a} : set nat)
#check ({a, a} : set nat)
#check ({a, 1, a} : set nat)
#check ({a} : set nat)
check { a // a > 0 }
#check { a // a > 0 }

2
tests/lean/def3.lean
View File

@@ -5,6 +5,6 @@ section
definition f : A → A :=
λ x, x
check f
#check f
end

14
tests/lean/def4.lean
View File

@@ -5,18 +5,18 @@ section
definition f : A → A :=
λ x, x
check f
check f (0:nat) -- error
#check f
#check f (0:nat) -- error
parameter {A}
definition g : A → A :=
λ x, x
check g
check g (0:nat) -- error
#check g
#check g (0:nat) -- error
end
check f
check f _ (0:nat)
check g 0
#check f
#check f _ (0:nat)
#check g 0

4
tests/lean/def4.lean.expected.out
View File

@@ -1,5 +1,5 @@
f : A → A
def4.lean:9:8: error: type mismatch at application
def4.lean:9:9: error: type mismatch at application
f 0
term
0
@@ -9,7 +9,7 @@ but is expected to have type
A
sorry : ?M_1
g : A → A
def4.lean:17:8: error: type mismatch at application
def4.lean:17:9: error: type mismatch at application
g 0
term
0

2
tests/lean/def_inaccessible_issue.lean
View File

@@ -14,4 +14,4 @@ definition map2 : ∀ {n}, bv n → bv n → bv n
| 0 nil nil := nil
| (n+1) (cons .n b1 v1) (cons .n b2 v2) := cons n (f b1 b2) (map2 v1 v2)
check map2.equations._eqn_2
#check map2.equations._eqn_2

10
tests/lean/def_ite_value.lean
View File

@@ -5,8 +5,8 @@ definition f : string → nat → nat
| "bye" 1 := 2
| _ _ := 3
vm_eval f "hello world" 1
vm_eval f "hello world" 2
vm_eval f "bye" 1
vm_eval f "bye" 2
vm_eval f "hello" 1
#eval f "hello world" 1
#eval f "hello world" 2
#eval f "bye" 1
#eval f "bye" 2
#eval f "hello" 1

12
tests/lean/elab1.lean
View File

@@ -7,19 +7,19 @@ definition boo.add := @add
set_option pp.all true
open foo boo
print raw subst -- subst is overloaded
print raw add -- add is overloaded
#print raw subst -- subst is overloaded
#print raw add -- add is overloaded
check @subst
#check @subst
check @@subst
#check @@subst
open eq
check subst
#check subst
constants a b : nat
constant H1 : a = b
constant H2 : a + b > 0
check eq.subst H1 H2
#check eq.subst H1 H2

8
tests/lean/elab1.lean.expected.out
View File

@@ -1,8 +1,8 @@
[choice boo.subst foo.subst]
[choice add boo.add foo.add]
elab1.lean:13:6: error: invalid '@', function is overloaded, use fully qualified names (overloads: boo.subst, foo.subst)
elab1.lean:15:6: error: invalid '@@', function is overloaded, use fully qualified names (overloads: boo.subst, foo.subst)
elab1.lean:19:6: error: invalid overloaded application, elaborator has special support for 'eq.subst' (it is handled as an "eliminator"), but this kind of constant cannot be overloaded (solution: use fully qualified names) (overloads: eq.subst, boo.subst, foo.subst)
elab1.lean:13:7: error: invalid '@', function is overloaded, use fully qualified names (overloads: boo.subst, foo.subst)
elab1.lean:15:7: error: invalid '@@', function is overloaded, use fully qualified names (overloads: boo.subst, foo.subst)
elab1.lean:19:7: error: invalid overloaded application, elaborator has special support for 'eq.subst' (it is handled as an "eliminator"), but this kind of constant cannot be overloaded (solution: use fully qualified names) (overloads: eq.subst, boo.subst, foo.subst)
sorry : ?M_1
elab1.lean:25:6: error: invalid 'eq.subst' application, elaborator has special support for this kind of application (it is handled as an "eliminator"), but the expected type must be known
elab1.lean:25:7: error: invalid 'eq.subst' application, elaborator has special support for this kind of application (it is handled as an "eliminator"), but the expected type must be known
sorry : ?M_1

8
tests/lean/elab11.lean
View File

@@ -3,14 +3,14 @@ constant bla.f : nat → nat
open boo bla
check f 1
#check f 1
set_option pp.full_names true
check (f 1 : nat)
#check (f 1 : nat)
check (f 1 : bool)
#check (f 1 : bool)
set_option pp.full_names false
check (f 1 : string)
#check (f 1 : string)

8
tests/lean/elab11.lean.expected.out
View File

@@ -1,12 +1,12 @@
elab11.lean:6:6: error: ambiguous overload, possible interpretations
elab11.lean:6:7: error: ambiguous overload, possible interpretations
bla.f 1
boo.f 1
Additional information:
elab11.lean:6:6: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because expected type was not available
elab11.lean:6:7: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because expected type was not available
sorry : ?M_1
bla.f 1 : ℕ
boo.f 1 : bool
elab11.lean:16:7: error: none of the overloads are applicable
elab11.lean:16:8: error: none of the overloads are applicable
error for bla.f
invalid overload, expression
f 1
@@ -23,7 +23,7 @@ has type
but is expected to have type
string
Additional information:
elab11.lean:16:7: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type, because failed to elaborate all candidates using the expected type
elab11.lean:16:8: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type, because failed to elaborate all candidates using the expected type
string
this can happen because, for example, coercions were not considered in the process
none of the overloads are applicable

10
tests/lean/elab12.lean
View File

@@ -1,14 +1,14 @@
check (take a : nat, have H : 0, from rfl a,
#check (take a : nat, have H : 0, from rfl a,
(H a a) : ∀ a : nat, a = a)
check (take a : nat, have H : a = a, from rfl a,
#check (take a : nat, have H : a = a, from rfl a,
(H a a) : ∀ a : nat, a = a)
check (take a : nat, have H : a = a, from a + 0,
#check (take a : nat, have H : a = a, from a + 0,
(H a a) : ∀ a : nat, a = a)
check (take a : nat, have H : a = a, from rfl,
#check (take a : nat, have H : a = a, from rfl,
(H a) : ∀ a : nat, a = a)
check (take a : nat, have H : a = a, from rfl,
#check (take a : nat, have H : a = a, from rfl,
H : ∀ a : nat, a = a)

12
tests/lean/elab12.lean.expected.out
View File

@@ -1,22 +1,22 @@
elab12.lean:1:30: error: type expected at
elab12.lean:1:31: error: type expected at
0
elab12.lean:1:38: error: function expected at
elab12.lean:1:39: error: function expected at
rfl
Additional information:
elab12.lean:1:38: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
elab12.lean:1:39: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
too many arguments
elab12.lean:2:2: error: function expected at
H
λ (a : ℕ), have H : sorry, from sorry, sorry : ∀ (a : ℕ), a = a
elab12.lean:4:42: error: function expected at
elab12.lean:4:43: error: function expected at
rfl
Additional information:
elab12.lean:4:42: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
elab12.lean:4:43: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
too many arguments
elab12.lean:5:2: error: function expected at
H
λ (a : ℕ), have H : a = a, from sorry, sorry : ∀ (a : ℕ), a = a
elab12.lean:7:44: error: invalid have-expression, expression
elab12.lean:7:45: error: invalid have-expression, expression
a + 0
has type
ℕ

2
tests/lean/elab13.lean
View File

@@ -1,6 +1,6 @@
open tactic list
check
#check
take c : name,
(
do {

2
tests/lean/elab14.lean
View File

@@ -1,3 +1,3 @@
set_option pp.all true
universe variables u
check λ (A B : Type u) (a : A) (b : B), a
#check λ (A B : Type u) (a : A) (b : B), a

2
tests/lean/elab15.lean
View File

@@ -1,7 +1,7 @@
open tactic
set_option pp.notation false
universe variables u
check
#check
λ (A : Type u) (a b c d : A) (H₁ : a = b) (H₂ : c = b) (H₃ : d = c),
have a = c, by do { transitivity, assumption, symmetry, assumption },
show a = d, by do { transitivity, this ← get_local "this", exact this, symmetry, assumption }

6
tests/lean/elab2.lean
View File

@@ -5,11 +5,11 @@ a
-- set_option trace.elaborator_detail true
set_option pp.all true
check foo 0 1
#check foo 0 1
definition bla {A B : Type*} (a₁ a₂ : A) (b : B) : A :=
a₁
check bla nat.zero tt 1
#check bla nat.zero tt 1
check bla 0 0 tt
#check bla 0 0 tt

2
tests/lean/elab2.lean.expected.out
View File

@@ -1,5 +1,5 @@
@foo.{0 0} nat nat nat.has_add (@zero.{0} nat nat.has_zero) (@one.{0} nat nat.has_one) : nat
elab2.lean:13:6: error: type mismatch at application
elab2.lean:13:7: error: type mismatch at application
@bla.{0 ?l_1} nat ?m_2 nat.zero bool.tt
term
bool.tt

2
tests/lean/elab3.lean
View File

@@ -3,4 +3,4 @@ open tactic
set_option pp.all true
check trace_state >> trace_state
#check trace_state >> trace_state

14
tests/lean/elab4.lean
View File

@@ -8,16 +8,16 @@ open boo foo bla
set_option pp.full_names true
check f 0 1 2
#check f 0 1 2
check f 0 1 2 3
#check f 0 1 2 3
check f 0 1
#check f 0 1
check f tt 2
#check f tt 2
check f tt ff tt
#check f tt ff tt
check f tt ff
#check f tt ff
check @foo.f _ _ 0 1
#check @foo.f _ _ 0 1

12
tests/lean/elab4.lean.expected.out
View File

@@ -1,5 +1,5 @@
boo.f 0 1 2 : ℕ
elab4.lean:13:6: error: none of the overloads are applicable
elab4.lean:13:7: error: none of the overloads are applicable
error for bla.f
failed to synthesize type class instance for
⊢ has_add bool
@@ -12,20 +12,20 @@ error for boo.f
function expected at
boo.f 0 1 2
Additional information:
elab4.lean:13:6: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because expected type was not available
elab4.lean:13:7: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because expected type was not available
sorry : ?M_1
elab4.lean:15:6: error: ambiguous overload, possible interpretations
elab4.lean:15:7: error: ambiguous overload, possible interpretations
foo.f 0 1
boo.f 0 1
Additional information:
elab4.lean:15:6: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because expected type was not available
elab4.lean:15:7: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because expected type was not available
sorry : ?M_1
foo.f bool.tt 2 : bool
bla.f bool.tt bool.ff bool.tt : bool → bool
elab4.lean:21:6: error: ambiguous overload, possible interpretations
elab4.lean:21:7: error: ambiguous overload, possible interpretations
bla.f bool.tt bool.ff
foo.f bool.tt bool.ff
Additional information:
elab4.lean:21:6: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because expected type was not available
elab4.lean:21:7: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because expected type was not available
sorry : ?M_1
foo.f 0 1 : ℕ

6
tests/lean/elab4b.lean
View File

@@ -6,8 +6,8 @@ definition bla.f (a b c d : bool) := a
open boo foo bla
check f 0 1 2 3
#check f 0 1 2 3
check f 0 1
#check f 0 1
check f tt ff
#check f tt ff

12
tests/lean/elab4b.lean.expected.out
View File

@@ -1,4 +1,4 @@
elab4b.lean:9:6: error: none of the overloads are applicable
elab4b.lean:9:7: error: none of the overloads are applicable
error for bla.f
failed to synthesize type class instance for
⊢ has_add bool
@@ -11,17 +11,17 @@ error for boo.f
function expected at
f 0 1 2
Additional information:
elab4b.lean:9:6: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because expected type was not available
elab4b.lean:9:7: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because expected type was not available
sorry : ?M_1
elab4b.lean:11:6: error: ambiguous overload, possible interpretations
elab4b.lean:11:7: error: ambiguous overload, possible interpretations
foo.f 0 1
boo.f 0 1
Additional information:
elab4b.lean:11:6: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because expected type was not available
elab4b.lean:11:7: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because expected type was not available
sorry : ?M_1
elab4b.lean:13:6: error: ambiguous overload, possible interpretations
elab4b.lean:13:7: error: ambiguous overload, possible interpretations
bla.f bool.tt bool.ff
foo.f bool.tt bool.ff
Additional information:
elab4b.lean:13:6: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because expected type was not available
elab4b.lean:13:7: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because expected type was not available
sorry : ?M_1

2
tests/lean/elab5.lean
View File

@@ -1,3 +1,3 @@
constant s : sum nat bool
check @eq.refl (sum nat bool) s
#check @eq.refl (sum nat bool) s

20
tests/lean/elab6.lean
View File

@@ -4,14 +4,14 @@ set_option pp.all true
constant F : ∀ {A : Type*} ⦃a : A⦄ {b : A} (c : A) ⦃e : A⦄, A → A → A
check H
check F
check F tt
check F tt tt
check F tt tt tt
#check H
#check F
#check F tt
#check F tt tt
#check F tt tt tt
check H
check F
check F tt
check F tt tt
check F tt tt tt
#check H
#check F
#check F tt
#check F tt tt
#check F tt tt tt

8
tests/lean/elab7.lean
View File

@@ -1,10 +1,10 @@
set_option pp.all true
set_option pp.purify_metavars false
check λ x : nat, x + 1
#check λ x : nat, x + 1
check λ x y : nat, x + y
#check λ x y : nat, x + y
check λ x y, x + y + 1
#check λ x y, x + y + 1
check λ x, (x + 1) :: []
#check λ x, (x + 1) :: []

6
tests/lean/elab8.lean
View File

@@ -3,8 +3,8 @@ set_option pp.implicit true
set_option pp.numerals false
set_option pp.binder_types true
check λ (A : Type*) [has_add A] [has_one A] [has_lt A] (a : A), a + 1
#check λ (A : Type*) [has_add A] [has_one A] [has_lt A] (a : A), a + 1
check λ (A : Type*) [has_add A] [has_one A] [has_lt A] (a : A) (H : a > 1), a + 1
#check λ (A : Type*) [has_add A] [has_one A] [has_lt A] (a : A) (H : a > 1), a + 1
check λ (A : Type*) [has_add A] [has_one A] [has_lt A] (a : A) (H₁ : a > 1) (H₂ : a < 5), a + 1
#check λ (A : Type*) [has_add A] [has_one A] [has_lt A] (a : A) (H₁ : a > 1) (H₂ : a < 5), a + 1

4
tests/lean/elab9.lean
View File

@@ -3,6 +3,6 @@ set_option pp.implicit true
set_option pp.numerals false
set_option pp.binder_types true
check λ (A : Type*) [has_add A] [has_zero A] (a : A) (H : a + 0 = a) [has_add A] (H : a = 0 + 0), a + a
#check λ (A : Type*) [has_add A] [has_zero A] (a : A) (H : a + 0 = a) [has_add A] (H : a = 0 + 0), a + a
check λ (a b : nat) (H : a > b) [has_lt nat], a < b
#check λ (a b : nat) (H : a > b) [has_lt nat], a < b

10
tests/lean/elab_error_recovery.lean
View File

@@ -11,11 +11,11 @@ def half_baked : ℕ → ℕ
-- nested elaboration errors
| _ := begin exact [] end
print half_baked._main
#print half_baked._main
eval half_baked 3
eval half_baked 5
vm_eval half_baked 3
#reduce half_baked 3
#reduce half_baked 5
#eval half_baked 3
-- type errors in binders
check ∀ x : nat.zero, x = x
#check ∀ x : nat.zero, x = x

2
tests/lean/elab_error_recovery.lean.expected.out
View File

@@ -43,6 +43,6 @@ def half_baked._main : ℕ → ℕ :=
2
nat.succ (nat.succ (nat.succ (nat.succ sorry)))
2
elab_error_recovery.lean:21:12: error: type expected at
elab_error_recovery.lean:21:13: error: type expected at
0
∀ (x : sorry), x = x : Prop

16
tests/lean/elab_meta2.lean
View File

@@ -1,29 +1,29 @@
print "parametric meta definition"
#print "parametric meta definition"
meta definition f {A : Type} : nat → A → A → A
| n a b := if n / 2 = 0 then a else f (n / 2) b a
vm_eval
#eval
if f 10 1 2 = 2 then "OK" else "FAILED"
namespace foo
print "parametric meta definition inside namespace"
#print "parametric meta definition inside namespace"
meta definition bla {A : Type} : nat → A → A → A
| n a b := if n / 2 = 0 then a else bla (n / 2) b a
vm_eval
#eval
if foo.bla 10 1 2 = 2 then "OK" else "FAILED"
end foo
namespace foo
section
print "meta definition inside parametric scope"
#print "meta definition inside parametric scope"
parameter {A : Type}
meta definition bah : nat → A → A → A
| n a b := if n / 2 = 0 then a else bah (n / 2) b a
end
vm_eval if foo.bah 10 1 2 = 2 then "OK" else "FAILED"
#eval if foo.bah 10 1 2 = 2 then "OK" else "FAILED"
end foo
print "private meta definition"
#print "private meta definition"
private meta definition hprv {A : Type} : nat → A → A → A
| n a b := if n / 2 = 0 then a else hprv (n / 2) b a
vm_eval
#eval
if hprv 10 1 2 = 2 then "OK" else "FAILED"

4
tests/lean/error_full_names.lean
View File

@@ -1,9 +1,9 @@
namespace foo
open nat
inductive nat : Type | zero, foosucc : nat → nat
check 0 + nat.zero --error
#check 0 + nat.zero --error
end foo
namespace foo
check nat.succ nat.zero --error
#check nat.succ nat.zero --error
end foo

6
tests/lean/error_full_names.lean.expected.out
View File

@@ -1,9 +1,9 @@
error_full_names.lean:4:6: error: failed to synthesize type class instance for
error_full_names.lean:4:7: error: failed to synthesize type class instance for
⊢ has_zero nat
error_full_names.lean:4:8: error: failed to synthesize type class instance for
error_full_names.lean:4:9: error: failed to synthesize type class instance for
⊢ has_add nat
0 + nat.zero : nat
error_full_names.lean:8:6: error: type mismatch at application
error_full_names.lean:8:7: error: type mismatch at application
nat.succ nat.zero
term
nat.zero

6
tests/lean/error_pos.lean
View File

@@ -6,11 +6,11 @@ begin
intros, trivial
end
check λ (A : Type) (B : A → Type) (b : B), true
#check λ (A : Type) (B : A → Type) (b : B), true
check λ (A : Type) (B : A → Type), B → true
#check λ (A : Type) (B : A → Type), B → true
check λ (A : Type) (B : A → Type) b, (b : B)
#check λ (A : Type) (B : A → Type) b, (b : B)
example {A : Type} {B : Type} {a₁ a₂ : B} {b₁ b₂ : A → B} : a₁ = a₂ → (∀ x, b₁ x = b₂ x) → (let x : A := a₁ in b₁ x) = (let x : A := a₂ in b₂ x) :=
sorry

6
tests/lean/error_pos.lean.expected.out
View File

@@ -3,13 +3,13 @@ error_pos.lean:1:39: error: type expected at
error_pos.lean:1:8: warning: declaration '_example' uses sorry
error_pos.lean:4:43: error: type expected at
B
error_pos.lean:9:39: error: type expected at
error_pos.lean:9:40: error: type expected at
B
λ (A : Type) (B : A → Type) (b : sorry), true : Π (A : Type), (A → Type) → sorry → Prop
error_pos.lean:11:35: error: type expected at
error_pos.lean:11:36: error: type expected at
B
λ (A : Type) (B : A → Type), sorry → true : Π (A : Type), (A → Type) → Prop
error_pos.lean:13:42: error: type expected at
error_pos.lean:13:43: error: type expected at
B
λ (A : Type) (B : A → Type) (b : sorry), b : Π (A : Type), (A → Type) → sorry → sorry
error_pos.lean:15:105: error: invalid let-expression, expression

2
tests/lean/eta_bug.lean
View File

@@ -1,4 +1,4 @@
--
eval λ (A : Type*) (x y : A) (H₁ : x = y) (H₂ : y = x), eq.trans H₁ H₂
#reduce λ (A : Type*) (x y : A) (H₁ : x = y) (H₂ : y = x), eq.trans H₁ H₂
-- Should not reduce to
-- λ (A : Type*) (x y : A), eq.trans

4
tests/lean/eval_expr_error.lean
View File

@@ -5,13 +5,13 @@ do a ← to_expr `(0),
v ← eval_expr A a,
return ()
run_command do
run_cmd do
a ← to_expr `(nat.add),
v ← eval_expr nat a,
trace v,
return ()
run_command do
run_cmd do
a ← to_expr `(λ x : nat, x + 1),
v ← (eval_expr nat a <|> trace "tactic failed" >> return 1),
trace v,

2
tests/lean/expr_quote.lean
View File

@@ -3,4 +3,4 @@ meta def f (α a : expr) := ```(@id %%α %%a)
meta def f (α a : expr) := ```(@id (%%α : Type 2) %%a)
set_option pp.universes true
print f
#print f

8
tests/lean/extra/print_tests.lean
View File

@@ -1,7 +1,7 @@
print notation
#print notation
print notation ∧ ∨
#print notation ∧ ∨
print notation if
#print notation if
print notation %
#print notation %

6
tests/lean/field_access.lean
View File

@@ -1,10 +1,10 @@
check list.map
#check list.map
variable l : list nat
check l~>1 -- Error l is not a structure
#check l~>1 -- Error l is not a structure
check (1, 2)~>5 -- Error insufficient fields
#check (1, 2)~>5 -- Error insufficient fields
example (l : list nat) : list nat :=
l~>forr (λ x, x + 1) -- Error there is no list.forr

4
tests/lean/field_access.lean.expected.out
View File

@@ -1,10 +1,10 @@
list.map : (?M_1 → ?M_2) → list ?M_1 → list ?M_2
field_access.lean:5:7: error: invalid projection, structure expected
field_access.lean:5:8: error: invalid projection, structure expected
l
has type
list ℕ
sorry : ?M_1
field_access.lean:7:12: error: invalid projection, structure has only 2 field(s)
field_access.lean:7:13: error: invalid projection, structure has only 2 field(s)
(1, 2)
which has type
?m_1 × ?m_2

16
tests/lean/fold.lean
View File

@@ -5,31 +5,31 @@ variables a b c : num
section
local notation `(` t:(foldr `, ` (e r, prod.mk e r)) `)` := t
check (a, false, b, true, c)
#check (a, false, b, true, c)
set_option pp.notation false
check (a, false, b, true, c)
#check (a, false, b, true, c)
end
section
local notation `(` t:(foldr `, ` (e r, prod.mk r e)) `)` := t
set_option pp.notation true
check (a, false, b, true, c)
#check (a, false, b, true, c)
set_option pp.notation false
check (a, false, b, true, c)
#check (a, false, b, true, c)
end
section
local notation `(` t:(foldl `, ` (e r, prod.mk r e)) `)` := t
set_option pp.notation true
check (a, false, b, true, c)
#check (a, false, b, true, c)
set_option pp.notation false
check (a, false, b, true, c)
#check (a, false, b, true, c)
end
section
local notation `(` t:(foldl `, ` (e r, prod.mk e r)) `)` := t
set_option pp.notation true
check (a, false, b, true, c)
#check (a, false, b, true, c)
set_option pp.notation false
check (a, false, b, true, c)
#check (a, false, b, true, c)
end

4
tests/lean/ftree.lean
View File

@@ -16,7 +16,7 @@ inductive ftree (A : Type) (B : Type) : Type
| node : (A → B → ftree) → (B → ftree) → ftree
set_option pp.universes true
check ftree
#check ftree
end implicit
@@ -27,5 +27,5 @@ inductive ftree (A : Type) (B : Type) : Type
| leafb : B → ftree
| node : (List A → ftree) → (B → ftree) → ftree
set_option pp.universes true
check ftree
#check ftree
end implicit2

6
tests/lean/hex_char.lean
View File

@@ -1,3 +1,3 @@
vm_eval #"\x41"
vm_eval #"\x42"
vm_eval #"\x43"
#eval #"\x41"
#eval #"\x42"
#eval #"\x43"

10
tests/lean/hex_numeral.lean
View File

@@ -1,5 +1,5 @@
vm_eval (0xff : nat)
vm_eval (0xffff : nat)
vm_eval (0xaa : nat)
vm_eval (0x10 : nat)
vm_eval (0x10000 : nat)
#eval (0xff : nat)
#eval (0xffff : nat)
#eval (0xaa : nat)
#eval (0x10 : nat)
#eval (0x10000 : nat)

2
tests/lean/hinst_lemmas1.lean
View File

@@ -3,7 +3,7 @@ axiom foo2 : ∀ (a b c : nat), b > a → b < c → a < c
axiom foo3 : ∀ (a b c : nat), b > a → b < c + c → a < c + c
run_command
run_cmd
do
hs ← return $ hinst_lemmas.mk,
h₁ ← hinst_lemma.mk_from_decl `foo1,

4
tests/lean/hinst_lemmas2.lean
View File

@@ -1,4 +1,4 @@
run_command mk_hinst_lemma_attr_set `attr_main [`attr1, `attr2] [`sattr1, `sattr2]
run_cmd mk_hinst_lemma_attr_set `attr_main [`attr1, `attr2] [`sattr1, `sattr2]
constant f : nat → nat
constant g : nat → nat → nat
@@ -20,4 +20,4 @@ attribute [attr2] gax4
attribute [attr_main] gax5
attribute [sattr1] gax6
run_command get_hinst_lemmas_for_attr `attr_main >>= hinst_lemmas.pp >>= tactic.trace
run_cmd get_hinst_lemmas_for_attr `attr_main >>= hinst_lemmas.pp >>= tactic.trace

Some files were not shown because too many files have changed in this diff Show More