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

fix(frontends/lean/structure_cmd): 'rec' must be marked as protected

Browse source
This commit is contained in:
Leonardo de Moura 2014-11-03 14:50:12 -08:00
parent 0f56b5f5b7
commit 594e3ea8fc
3 changed files with 14 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/frontends/lean/structure_cmd.cpp
View file

@ -21,6 +21,7 @@ Author: Leonardo de Moura
#include "library/reducible.h"
#include "library/unifier.h"
#include "library/module.h"
#include "library/protected.h"
#include "library/definitional/rec_on.h"
#include "library/definitional/induction_on.h"
#include "library/definitional/cases_on.h"
@ -524,8 +525,11 @@ struct structure_cmd_fn {
inductive::inductive_decl decl(m_name, structure_type, to_list(intro));
m_env = module::add_inductive(m_env, lnames, m_params.size(), to_list(decl));
save_info(m_name, "structure", m_name_pos);
save_info(inductive::get_elim_name(m_name), "recursor", m_name_pos);
name rec_name = inductive::get_elim_name(m_name);
save_info(rec_name, "recursor", m_name_pos);
save_info(m_mk, "intro", m_mk_pos);
m_env = add_namespace(m_env, m_name);
m_env = add_protected(m_env, rec_name);
}
void declare_projections() {

8
tests/lean/record_rec_protected.lean Normal file
View file

@ -0,0 +1,8 @@
import logic data.unit
structure point (A : Type) (B : Type) :=
mk :: (x : A) (y : B)
open point
check rec -- error, rec is protected

1
tests/lean/record_rec_protected.lean.expected.out Normal file
View file

@ -0,0 +1 @@
record_rec_protected.lean:8:6: error: unknown identifier 'rec'