michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(frontends/lean/builtin_cmds): add 'variable' command family

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-13 15:13:32 -07:00
parent ce259e6265
commit 01cecb76db
11 changed files with 414 additions and 88 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

168
src/frontends/lean/builtin_cmds.cpp
View file

@ -4,38 +4,138 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <algorithm>
#include "util/sstream.h"
#include "kernel/type_checker.h"
#include "library/io_state_stream.h"
#include "library/scoped_ext.h"
#include "library/aliases.h"
#include "library/locals.h"
#include "frontends/lean/parser.h"
namespace lean {
static name g_raw("raw");
static name g_llevel_curly(".{");
static name g_rcurly("}");
static name g_colon(":");
static void check_atomic(name const & n) {
if (!n.is_atomic())
throw exception(sstream() << "invalid declaration name '" << n << "', identifier must be atomic");
}
environment universe_cmd(parser & p) {
if (p.curr_is_identifier()) {
name n = p.get_name_val();
check_atomic(n);
p.next();
environment env = p.env();
if (in_section(env)) {
p.add_local_level(n, mk_param_univ(n));
} else {
name const & ns = get_namespace(env);
name full_n = ns + n;
env = env.add_universe(full_n);
if (!ns.is_anonymous())
env = add_alias(env, n, mk_global_univ(full_n));
}
return env;
name n = p.check_id_next("invalid universe declaration, identifier expected");
check_atomic(n);
environment env = p.env();
if (in_section(env)) {
p.add_local_level(n, mk_param_univ(n));
} else {
throw parser_error("invalid universe declaration, identifier expected", p.cmd_pos());
name const & ns = get_namespace(env);
name full_n = ns + n;
env = env.add_universe(full_n);
if (!ns.is_anonymous())
env = add_alias(env, n, mk_global_univ(full_n));
}
return env;
}
static void check_in_section(parser const & p) {
if (!in_section(p.env()))
throw exception(sstream() << "invalid command, it must be used in a section");
}
static void parse_univ_params(parser & p, buffer<name> & ps) {
if (p.curr_is_token(g_llevel_curly)) {
p.next();
while (!p.curr_is_token(g_rcurly)) {
name l = p.check_id_next("invalid universe parameter, identifier expected");
p.add_local_level(l, mk_param_univ(l));
ps.push_back(l);
}
p.next();
}
}
struct local_scope_if_not_section {
parser & m_p;
local_scope_if_not_section(parser & p):m_p(p) {
if (!in_section(p.env()))
p.push_local_scope();
}
~local_scope_if_not_section() {
if (!in_section(m_p.env()))
m_p.pop_local_scope();
}
};
static void update_parameters(buffer<name> & ls_buffer, name_set const & found, parser const & p) {
unsigned old_sz = ls_buffer.size();
found.for_each([&](name const & n) {
if (std::find(ls_buffer.begin(), ls_buffer.begin() + old_sz, n) == ls_buffer.begin() + old_sz)
ls_buffer.push_back(n);
});
std::sort(ls_buffer.begin(), ls_buffer.end(), [&](name const & n1, name const & n2) {
return *p.get_local_level_index(n1) < *p.get_local_level_index(n2);
});
}
environment variable_cmd_core(parser & p, bool is_axiom, binder_info const & bi) {
name n = p.check_id_next("invalid declaration, identifier expected");
check_atomic(n);
buffer<name> ls_buffer;
buffer<parameter> ps;
if (p.curr_is_token(g_llevel_curly) && in_section(p.env()))
throw parser_error("invalid declaration, axioms/parameters occurring in sections cannot be universe polymorphic", p.pos());
local_scope_if_not_section scope(p);
parse_univ_params(p, ls_buffer);
p.set_type_use_placeholder(false);
if (!p.curr_is_token(g_colon))
p.parse_binders(ps);
p.check_token_next(g_colon, "invalid declaration, ':' expected");
expr type = p.parse_scoped_expr(ps);
level_param_names ls;
if (in_section(p.env())) {
ls = to_level_param_names(collect_univ_params(type));
} else {
update_parameters(ls_buffer, collect_univ_params(type), p);
ls = to_list(ls_buffer.begin(), ls_buffer.end());
}
type = p.pi_abstract(ps, type);
type = p.elaborate(type, ls);
if (in_section(p.env())) {
p.add_local_expr(n, mk_local(n, n, type), bi);
return p.env();
} else {
environment env = p.env();
name const & ns = get_namespace(env);
name full_n = ns + n;
if (is_axiom)
env = env.add(check(env, mk_axiom(full_n, ls, type)));
else
env = env.add(check(env, mk_var_decl(full_n, ls, type)));
if (!ns.is_anonymous())
env = add_alias(env, n, mk_constant(full_n));
return env;
}
}
environment variable_cmd(parser & p) {
return variable_cmd_core(p, false, binder_info());
}
environment axiom_cmd(parser & p) {
return variable_cmd_core(p, true, binder_info());
}
environment implicit_variable_cmd(parser & p) {
check_in_section(p);
return variable_cmd_core(p, false, mk_implicit_binder_info());
}
environment implicit_axiom_cmd(parser & p) {
check_in_section(p);
return variable_cmd_core(p, true, mk_implicit_binder_info());
}
environment cast_variable_cmd(parser & p) {
check_in_section(p);
return variable_cmd_core(p, false, mk_cast_binder_info());
}
environment print_cmd(parser & p) {
@ -58,14 +158,9 @@ environment section_cmd(parser & p) {
}
environment namespace_cmd(parser & p) {
if (p.curr_is_identifier()) {
name n = p.get_name_val();
check_atomic(n);
p.next();
return push_scope(p.env(), p.ios(), n);
} else {
throw parser_error("invalid namespace declaration, identifier expected", p.cmd_pos());
}
name n = p.check_id_next("invalid namespace declaration, identifier expected");
check_atomic(n);
return push_scope(p.env(), p.ios(), n);
}
environment end_scoped_cmd(parser & p) {
@ -74,13 +169,28 @@ environment end_scoped_cmd(parser & p) {
return pop_scope(p.env());
}
environment check_cmd(parser & p) {
expr e = p.parse_expr();
level_param_names ls = to_level_param_names(collect_univ_params(e));
e = p.elaborate(e, ls);
expr type = type_checker(p.env()).check(e, ls);
p.regular_stream() << e << " : " << type << endl;
return p.env();
}
cmd_table init_cmd_table() {
cmd_table r;
add_cmd(r, cmd_info("print", "print a string", print_cmd));
add_cmd(r, cmd_info("universe", "declare a global universe level", universe_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("print", "print a string", print_cmd));
add_cmd(r, cmd_info("universe", "declare a global universe level", universe_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("variable", "declare a new parameter", variable_cmd));
add_cmd(r, cmd_info("{variable}", "declare a new implict parameter", implicit_variable_cmd));
add_cmd(r, cmd_info("[variable]", "declare a new cast parameter", cast_variable_cmd));
add_cmd(r, cmd_info("axiom", "declare a new axiom", axiom_cmd));
add_cmd(r, cmd_info("{axiom}", "declare a new implicit axiom", implicit_axiom_cmd));
add_cmd(r, cmd_info("check", "type check given expression, and display its type", check_cmd));
return r;
}

5
src/frontends/lean/builtin_exprs.cpp
View file

@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "frontends/lean/builtin_exprs.h"
#include "frontends/lean/token_table.h"
#include "frontends/lean/parser.h"
namespace lean {
@ -38,8 +39,8 @@ parse_table init_nud_table() {
}
parse_table init_led_table() {
parse_table r;
// TODO(Leo)
parse_table r(false);
r.add({transition("->", mk_expr_action(get_arrow_prec() + 1))}, mk_arrow(Var(0), Var(2)));
return r;
}
}

54
src/frontends/lean/parser.cpp
View file

@ -191,6 +191,14 @@ void parser::check_token_next(name const & tk, char const * msg) {
next();
}
name parser::check_id_next(char const * msg) {
if (!curr_is_identifier())
throw parser_error(msg, pos());
name r = get_name_val();
next();
return r;
}
expr parser::mk_app(expr fn, expr arg, pos_info const & p) {
return save_pos(::lean::mk_app(fn, arg), p);
}
@ -213,8 +221,8 @@ void parser::add_local_level(name const & n, level const & l) {
m_local_level_decls.insert(n, local_level_entry(l, m_local_level_decls.size()));
}
void parser::add_local_expr(name const & n, expr const & e) {
m_local_decls.insert(n, local_entry(e, m_local_decls.size()));
void parser::add_local_expr(name const & n, expr const & e, binder_info const & bi) {
m_local_decls.insert(n, local_entry(parameter(pos(), e, bi), m_local_decls.size()));
}
void parser::add_local(expr const & e) {
@ -222,6 +230,22 @@ void parser::add_local(expr const & e) {
add_local_expr(local_pp_name(e), e);
}
optional<unsigned> parser::get_local_level_index(name const & n) const {
auto it = m_local_level_decls.find(n);
if (it != m_local_level_decls.end())
return optional<unsigned>(it->second.second);
else
return optional<unsigned>();
}
optional<unsigned> parser::get_local_index(name const & n) const {
auto it = m_local_decls.find(n);
if (it != m_local_decls.end())
return optional<unsigned>(it->second.second);
else
return optional<unsigned>();
}
/** \brief Parse a sequence of identifiers <tt>ID*</tt>. Store the result in \c result. */
void parser::parse_names(buffer<std::pair<pos_info, name>> & result) {
while (curr_is_identifier()) {
@ -372,6 +396,11 @@ expr parser::mk_Type() {
}
}
expr parser::elaborate(expr const & e, level_param_names const &) {
// TODO(Leo):
return e;
}
/** \brief Parse <tt>ID ':' expr</tt>, where the expression represents the type of the identifier. */
parameter parser::parse_binder_core(binder_info const & bi) {
auto p = pos();
@ -576,7 +605,7 @@ expr parser::parse_id() {
auto it1 = m_local_decls.find(id);
// locals
if (it1 != m_local_decls.end())
return copy_with_new_pos(it1->second.first, p);
return copy_with_new_pos(it1->second.first.m_local, p);
buffer<level> lvl_buffer;
auto p_lvl = pos();
levels ls;
@ -673,18 +702,15 @@ expr parser::parse_expr(unsigned rbp) {
return left;
}
expr parser::parse_scoped_expr(unsigned num_locals, expr const * locals, unsigned rbp) {
local_decls::mk_scope scope(m_local_decls);
for (unsigned i = 0; i < num_locals; i++)
add_local(locals[i]);
return parse_expr(rbp);
}
expr parser::parse_scoped_expr(unsigned num_params, parameter const * ps, unsigned rbp) {
local_decls::mk_scope scope(m_local_decls);
for (unsigned i = 0; i < num_params; i++)
add_local(ps[i].m_local);
return parse_expr(rbp);
if (num_params == 0) {
return parse_expr(rbp);
} else {
local_decls::mk_scope scope(m_local_decls);
for (unsigned i = 0; i < num_params; i++)
add_local(ps[i].m_local);
return parse_expr(rbp);
}
}
expr parser::abstract(unsigned num_params, parameter const * ps, expr const & e, bool lambda) {

84
src/frontends/lean/parser.h
View file

@ -43,7 +43,7 @@ struct parser_error : public exception {
struct interrupt_parser {};
class parser {
typedef std::pair<expr, unsigned> local_entry;
typedef std::pair<parameter, unsigned> local_entry;
typedef std::pair<level, unsigned> local_level_entry;
typedef scoped_map<name, local_entry, name_hash, name_eq> local_decls;
typedef scoped_map<name, local_level_entry, name_hash, name_eq> local_level_decls;
@ -133,42 +133,6 @@ public:
io_state const & ios() const { return m_ios; }
script_state * ss() const { return m_ss; }
void parse_names(buffer<std::pair<pos_info, name>> & result);
unsigned parse_small_nat();
level parse_level(unsigned rbp = 0);
parameter parse_binder();
void parse_binders(buffer<parameter> & r);
expr parse_expr(unsigned rbp = 0);
expr parse_scoped_expr(unsigned num_locals, expr const * locals, unsigned rbp = 0);
expr parse_scoped_expr(unsigned num_params, parameter const * ps, unsigned rbp = 0);
expr parse_scoped_expr(buffer<parameter> & ps, unsigned rbp = 0) { return parse_scoped_expr(ps.size(), ps.data(), rbp); }
expr abstract(unsigned num_params, parameter const * ps, expr const & e, bool lambda = true);
expr abstract(buffer<parameter> const & ps, expr const & e, bool lambda = true) { return abstract(ps.size(), ps.data(), e, lambda); }
tactic parse_tactic(unsigned rbp = 0);
void push_local_scope();
void pop_local_scope();
void add_local_level(name const & n, level const & l);
void add_local_expr(name const & n, expr const & e);
void add_local(expr const & t);
/**
\brief Specify how the method mk_Type behaves. When <tt>set_type_use_placeholder(true)</tt>, then
it returns <tt>'Type.{_}'</tt>, where '_' is placeholder that instructs the Lean elaborator to
automalically infer a universe level expression for '_'. When <tt>set_type_use_placeholder(false)</tt>,
then it returns <tt>'Type.{l}'</tt>, where \c l is a fresh universe level parameter.
The new parameter is automatically added to \c m_local_level_decls.
\remark When the parse is created the flag is set to false.
\remark Before parsing a command, the parser automatically "caches" the current value, and
restores it after the command is parsed (or aborted).
*/
void set_type_use_placeholder(bool f) { m_type_use_placeholder = f; }
expr mk_Type();
/** \brief Return the current position information */
pos_info pos() const { return pos_info(m_scanner.get_line(), m_scanner.get_pos()); }
expr save_pos(expr e, pos_info p);
@ -191,6 +155,8 @@ public:
bool curr_is_token(name const & tk) const;
/** \brief Check current token, and move to next characther, throw exception if current token is not \c tk. */
void check_token_next(name const & tk, char const * msg);
/** \brief Check if the current token is an identifier, if it is return it and move to next token, otherwise throw an exception. */
name check_id_next(char const * msg);
mpq const & get_num_val() const { return m_scanner.get_num_val(); }
name const & get_name_val() const { return m_scanner.get_name_val(); }
@ -201,6 +167,50 @@ public:
regular regular_stream() const { return regular(env(), ios()); }
diagnostic diagnostic_stream() const { return diagnostic(env(), ios()); }
void parse_names(buffer<std::pair<pos_info, name>> & result);
unsigned parse_small_nat();
level parse_level(unsigned rbp = 0);
parameter parse_binder();
void parse_binders(buffer<parameter> & r);
expr parse_expr(unsigned rbp = 0);
expr parse_scoped_expr(unsigned num_params, parameter const * ps, unsigned rbp = 0);
expr parse_scoped_expr(buffer<parameter> & ps, unsigned rbp = 0) { return parse_scoped_expr(ps.size(), ps.data(), rbp); }
expr abstract(unsigned num_params, parameter const * ps, expr const & e, bool lambda = true);
expr abstract(buffer<parameter> const & ps, expr const & e, bool lambda = true) { return abstract(ps.size(), ps.data(), e, lambda); }
expr lambda_abstract(buffer<parameter> const & ps, expr const & e) { return abstract(ps, e, true); }
expr pi_abstract(buffer<parameter> const & ps, expr const & e) { return abstract(ps, e, false); }
tactic parse_tactic(unsigned rbp = 0);
void push_local_scope();
void pop_local_scope();
struct local_scope { parser & m_p; local_scope(parser & p):m_p(p) { p.push_local_scope(); } ~local_scope() { m_p.pop_local_scope(); } };
void add_local_level(name const & n, level const & l);
void add_local_expr(name const & n, expr const & e, binder_info const & bi = binder_info());
void add_local(expr const & t);
/** \brief Position of the local level declaration named \c n in the sequence of local level decls. */
optional<unsigned> get_local_level_index(name const & n) const;
/** \brief Position of the local declaration named \c n in the sequence of local decls. */
optional<unsigned> get_local_index(name const & n) const;
/**
\brief Specify how the method mk_Type behaves. When <tt>set_type_use_placeholder(true)</tt>, then
it returns <tt>'Type.{_}'</tt>, where '_' is placeholder that instructs the Lean elaborator to
automalically infer a universe level expression for '_'. When <tt>set_type_use_placeholder(false)</tt>,
then it returns <tt>'Type.{l}'</tt>, where \c l is a fresh universe level parameter.
The new parameter is automatically added to \c m_local_level_decls.
\remark When the parse is created the flag is set to false.
\remark Before parsing a command, the parser automatically "caches" the current value, and
restores it after the command is parsed (or aborted).
*/
void set_type_use_placeholder(bool f) { m_type_use_placeholder = f; }
expr mk_Type();
expr elaborate(expr const & e, level_param_names const &);
/** parse all commands in the input stream */
bool operator()() { return parse_commands(); }
};

17
src/frontends/lean/token_table.cpp
View file

@ -8,6 +8,8 @@ Author: Leonardo de Moura
#include "frontends/lean/token_table.h"
namespace lean {
static unsigned g_arrow_prec = 25;
unsigned get_arrow_prec() { return g_arrow_prec; }
token_table add_command_token(token_table const & s, char const * token) {
return insert(s, token, token_info(token));
}
@ -41,25 +43,28 @@ static char const * g_forall_unicode = "\u2200";
static char const * g_arrow_unicode = "\u2192";
static char const * g_cup = "\u2294";
token_table init_token_table() {
token_table t;
char const * builtin[] = {"fun", "Pi", "let", "in", "have", "show", "by", "from", "(", ")", "{", "}", "[", "]",
".{", "Type", "...", ",", ".", ":", "calc", ":=", "--", "(*", "(--", "->",
".{", "Type", "...", ",", ".", ":", "calc", ":=", "--", "(*", "(--",
"proof", "qed", "private", "raw", "Bool", "+", g_cup, nullptr};
char const * commands[] = {"theorem", "axiom", "variable", "definition", "evaluate", "check",
"print", "variables", "end", "namespace", "section", "import",
char const * commands[] = {"theorem", "axiom", "variable", "definition", "{axiom}", "{variable}", "[variable]",
"variables", "{variables}", "[variables]",
"evaluate", "check", "print", "end", "namespace", "section", "import",
"abbreviation", "inductive", "record", "structure", "module", "universe",
nullptr};
std::pair<char const *, char const *> aliases[] =
{{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"},
{g_arrow_unicode, "->"}, {nullptr, nullptr}};
{nullptr, nullptr}};
std::pair<char const *, char const *> cmd_aliases[] =
{{"parameter", "variable"}, {"parameters", "variables"}, {"lemma", "theorem"},
{"hypothesis", "axiom"}, {"conjecture", "axiom"}, {"corollary", "theorem"},
{"{parameter}", "{variable}"}, {"{parameters}", "{variables}"},
{"[parameter]", "[variable]"}, {"[parameters]", "[variables]"},
{"{hypothesis}", "{axiom}"}, {"{conjecture}", "{axiom}"},
{nullptr, nullptr}};
auto it = builtin;
@ -67,6 +72,7 @@ token_table init_token_table() {
t = add_token(t, *it);
it++;
}
t = add_token(t, "->", get_arrow_prec());
it = commands;
while (*it) {
@ -79,6 +85,7 @@ token_table init_token_table() {
t = add_token(t, it2->first, it2->second);
it2++;
}
t = add_token(t, g_arrow_unicode, "->", get_arrow_prec());
it2 = cmd_aliases;
while (it2->first) {

1
src/frontends/lean/token_table.h
View file

@ -12,6 +12,7 @@ Author: Leonardo de Moura
#include "util/lua.h"
namespace lean {
unsigned get_arrow_prec();
class token_info {
bool m_command;
name m_value;

2
src/library/CMakeLists.txt
View file

@ -3,7 +3,7 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp
resolve_macro.cpp kernel_serializer.cpp max_sharing.cpp
normalize.cpp shared_environment.cpp module.cpp coercion.cpp
private.cpp placeholder.cpp aliases.cpp level_names.cpp
update_declaration.cpp choice.cpp scoped_ext.cpp)
update_declaration.cpp choice.cpp scoped_ext.cpp locals.cpp)
# hop_match.cpp)
target_link_libraries(library ${LEAN_LIBS})

65
src/library/locals.cpp Normal file
View file

@ -0,0 +1,65 @@
/*
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "util/name_set.h"
#include "kernel/expr.h"
#include "kernel/for_each_fn.h"
namespace lean {
void collect_univ_params_core(level const & l, name_set & r) {
for_each(l, [&](level const & l) {
if (!has_param(l))
return false;
if (is_param(l))
r.insert(param_id(l));
return true;
});
}
name_set collect_univ_params(expr const & e, name_set const & ls) {
if (!has_param_univ(e)) {
return ls;
} else {
name_set r = ls;
for_each(e, [&](expr const & e, unsigned) {
if (!has_param_univ(e)) {
return false;
} else if (is_sort(e)) {
collect_univ_params_core(sort_level(e), r);
} else if (is_constant(e)) {
for (auto const & l : const_levels(e))
collect_univ_params_core(l, r);
}
return true;
});
return r;
}
}
level_param_names to_level_param_names(name_set const & ls) {
level_param_names r;
ls.for_each([&](name const & n) {
r = level_param_names(n, r);
});
return r;
}
name_set collect_locals(expr const & e, name_set const & ls) {
if (!has_local(e)) {
return ls;
} else {
name_set r = ls;
for_each(e, [&](expr const & e, unsigned) {
if (!has_local(e))
return false;
if (is_local(e))
r.insert(mlocal_name(e));
return true;
});
return r;
}
}
}

14
src/library/locals.h Normal file
View file

@ -0,0 +1,14 @@
/*
Copyright (c) 2014 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/name_set.h"
#include "kernel/expr.h"
namespace lean {
name_set collect_univ_params(expr const & e, name_set const & ls = name_set());
name_set collect_locals(expr const & e, name_set const & ls = name_set());
level_param_names to_level_param_names(name_set const & ls);
}

58
tests/lean/t4.lean Normal file
View file

@ -0,0 +1,58 @@
variable N : Type.{1}
check N
variable a : N
check a
check Bool → Bool
variable F.{l} : Type.{l} → Type.{l}
check F.{2}
universe u
check F.{u}
variable vec.{l} (A : Type.{l}) (n : N) : Type.{l}
variable f (a b : N) : N
variable len.{l} (A : Type.{l}) (n : N) (v : vec.{l} A n) : N
check f
check len.{1}
section
variable A : Type
variable B : Bool
hypothesis H : B
{parameter} C : Type
check B -> B
check A → A
check C
end
check A -- Error: A is part of the section
variable R : Type → Type
check R.{1 0}
check fun x y : N, x
namespace tst
variable N : Type.{2}
variable M : Type.{2}
print raw N -- Two possible interpretations N and tst.N
print raw tst.N -- Only one interpretation
end
print raw N -- Only one interpretation
namespace foo
variable M : Type.{3}
print raw M -- Only one interpretation
end
check tst.M
check foo.M
namespace foo
check M
end
check M -- Error
print "ok"
(*
local env = get_env()
print("Declarations:")
env:for_each_decl(function(d) print(d:name()) end)
print("-------------")
*)
universe l_1
variable T1 : Type -- T1 parameter is going to be called l_2

34
tests/lean/t4.lean.expected.out Normal file
View file

@ -0,0 +1,34 @@
N : Type
a : N
Bool -> Bool : Type
F.{2} : Type.{2} -> Type.{2}
F.{u} : Type.{u} -> Type.{u}
f : N -> N -> N
len.{1} : Pi (A : Type) (n : N) (v : vec.{1} A n), N
B -> B : Bool
A -> A : Type.{l_1}
C : Type.{l_2}
t4.lean:24:6: error: unknown identifier 'A'
R.{1 0} : Type -> Bool
fun (x : N) (y : N), x : N -> N -> N
choice N tst.N
tst.N
N
foo.M
tst.M : Type.{2}
foo.M : Type.{3}
foo.M : Type.{3}
t4.lean:47:6: error: unknown identifier 'M'
ok
Declarations:
tst.M
tst.N
N
a
F
R
len
vec
f
foo.M
-------------