Skip to content
This repository has been archived by the owner on Oct 14, 2023. It is now read-only.

Commit

Permalink
WIP
Browse files Browse the repository at this point in the history
  • Loading branch information
@Kha
Kha committed Mar 27, 2017
1 parent 964187f commit 8c847d5
Showing 1 changed file with 7 additions and 1 deletion.
8 changes: 7 additions & 1 deletion src/library/module.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -314,10 +314,16 @@ struct inductive_modification : public modification {
LEAN_MODIFICATION("ind")

inductive::certified_inductive_decl m_decl;
unsigned m_trust_lvl = LEAN_BELIEVER_TRUST_LEVEL + 1;

inductive_modification(inductive::certified_inductive_decl const & decl) : m_decl(decl) {}

inductive_modification(inductive::certified_inductive_decl const & decl, unsigned trust_lvl) :
m_decl(decl), m_trust_lvl(trust_lvl) {}

void perform(environment & env) const override {
if (m_trust_lvl > env.trust_lvl()) {
m_decl = unfold_untrusted_macros(env, decl);
}
env = m_decl.add(env);
}

Expand Down

2 comments on commit 8c847d5

@gebner
Copy link
Member

@gebner gebner commented on 8c847d5 Mar 27, 2017

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Did you get problems here when importing olean files from another trust level? If so, I think we should handle this case uniformly in both the decl_modification and the inductive_modification. In the decl_modification we store the original trust level inside the modification (and in the olean file), and expand the macros if the new environment has a lower trust level. See here.

@Kha
Copy link
Member Author

@Kha Kha commented on 8c847d5 Mar 27, 2017

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sorry, that was just a temporary commit when moving from laptop to work PC :) . I've now copied the decl_modification implementation, which should fix the last failing test.

Please sign in to comment.