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

fix(frontends/lean/decl_cmds): allow private transparent definitions

Browse source 
Example:
section
  universe l
  private definition T := Type.{max 1 l}
  ...
end
This commit is contained in:
Leonardo de Moura 2014-10-02 07:56:01 -07:00
parent 153e3927ac
commit 5bd8e9d141
1 changed files with 8 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/frontends/lean/decl_cmds.cpp
View file

@ -369,15 +369,21 @@ environment theorem_cmd(parser & p) {
}
environment private_definition_cmd(parser & p) {
bool is_theorem = false;
if (p.curr_is_token_or_id(get_definition_tk())) {
bool is_opaque = false;
if (p.curr_is_token_or_id(get_opaque_tk())) {
is_opaque = true;
p.next();
p.check_token_next(get_definition_tk(), "invalid 'private' definition, 'definition' expected");
} else if (p.curr_is_token_or_id(get_definition_tk())) {
p.next();
} else if (p.curr_is_token_or_id(get_theorem_tk())) {
p.next();
is_theorem = true;
is_opaque = true;
} else {
throw parser_error("invalid 'private' definition/theorem, 'definition' or 'theorem' expected", p.pos());
}
return definition_cmd_core(p, is_theorem, true, true, false);
return definition_cmd_core(p, is_theorem, is_opaque, true, false);
}
environment protected_definition_cmd(parser & p) {
bool is_theorem = false;