max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(frontends/lean/definition_cmds): create theorem when keyword 'theorem' is used

Browse source
This commit is contained in:
Leonardo de Moura 2016-09-19 14:48:16 -07:00
parent 9a967001be
commit ba5d608386
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/frontends/lean/definition_cmds.cpp
View file

@ -322,7 +322,9 @@ declare_definition(parser & p, environment const & env, def_cmd_kind kind, buffe
val = fix_rec_fn_name(val, c_name, c_real_name);
bool use_conv_opt = true;
bool is_trusted = kind != MetaDefinition;
auto def = mk_definition(new_env, c_real_name, to_list(lp_names), type, val, use_conv_opt, is_trusted);
auto def = kind == Theorem ?
mk_theorem(c_real_name, to_list(lp_names), type, val) :
mk_definition(new_env, c_real_name, to_list(lp_names), type, val, use_conv_opt, is_trusted);
auto cdef = check(p, new_env, c_name, def, pos);
new_env = module::add(new_env, cdef);