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

chore(library/blast): use "override" consistently for proof_step objects

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-16 18:30:59 -08:00
parent 38436468e2
commit 4dc27fb43b
7 changed files with 7 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/blast/backward_action.cpp
View file

@ -24,7 +24,7 @@ struct backward_proof_step_cell : public proof_step_cell {
virtual ~backward_proof_step_cell() {} virtual ~backward_proof_step_cell() {}
virtual action_result resolve(expr const & pr) const { virtual action_result resolve(expr const & pr) const override {
state & s = curr_state(); state & s = curr_state();
s.set_branch(m_branch); s.set_branch(m_branch);
expr mvar = head(m_mvars); expr mvar = head(m_mvars);

2
src/library/blast/intros_action.cpp
View file

@ -15,7 +15,7 @@ namespace blast {
struct intros_proof_step_cell : public proof_step_cell { struct intros_proof_step_cell : public proof_step_cell {
list<expr> m_new_hs; list<expr> m_new_hs;
virtual ~intros_proof_step_cell() {} virtual ~intros_proof_step_cell() {}
virtual action_result resolve(expr const & pr) const { virtual action_result resolve(expr const & pr) const override {
expr new_pr = mk_proof_lambda(curr_state(), m_new_hs, pr); expr new_pr = mk_proof_lambda(curr_state(), m_new_hs, pr);
return action_result::solved(new_pr); return action_result::solved(new_pr);
} }

2
src/library/blast/no_confusion_action.cpp
View file

@ -18,7 +18,7 @@ struct no_confusion_proof_step_cell : public proof_step_cell {
m_I_name(I_name), m_target(t), m_eq_href(e), m_num_new_eqs(n) {} m_I_name(I_name), m_target(t), m_eq_href(e), m_num_new_eqs(n) {}
virtual ~no_confusion_proof_step_cell() {} virtual ~no_confusion_proof_step_cell() {}
virtual action_result resolve(expr const & pr) const { virtual action_result resolve(expr const & pr) const override {
try { try {
expr it = pr; expr it = pr;
bool skip = true; bool skip = true;

2
src/library/blast/recursor_action.cpp
View file

@ -63,7 +63,7 @@ struct recursor_proof_step_cell : public proof_step_cell {
virtual ~recursor_proof_step_cell() {} virtual ~recursor_proof_step_cell() {}
virtual action_result resolve(expr const & pr) const { virtual action_result resolve(expr const & pr) const override {
state & s = curr_state(); state & s = curr_state();
s.set_branch(m_branch); s.set_branch(m_branch);
if (!m_dep) { if (!m_dep) {

2
src/library/blast/revert_action.cpp
View file

@ -15,7 +15,7 @@ struct revert_proof_step_cell : public proof_step_cell {
virtual ~revert_proof_step_cell() {} virtual ~revert_proof_step_cell() {}
virtual action_result resolve(expr const & pr) const { virtual action_result resolve(expr const & pr) const override {
expr new_pr = mk_app(pr, m_hs); expr new_pr = mk_app(pr, m_hs);
return action_result::solved(new_pr); return action_result::solved(new_pr);
} }

2
src/library/blast/simplify_actions.cpp
View file

@ -24,7 +24,7 @@ public:
virtual ~simplify_target_proof_step_cell() {} virtual ~simplify_target_proof_step_cell() {}
virtual action_result resolve(expr const & pr) const { virtual action_result resolve(expr const & pr) const override {
try { try {
app_builder & b = get_app_builder(); app_builder & b = get_app_builder();
if (m_iff) if (m_iff)

2
src/library/blast/subst_action.cpp
View file

@ -21,7 +21,7 @@ struct subst_proof_step_cell : public proof_step_cell {
m_target(t), m_eq_href(e), m_rhs(r), m_dep(d) {} m_target(t), m_eq_href(e), m_rhs(r), m_dep(d) {}
virtual ~subst_proof_step_cell() {} virtual ~subst_proof_step_cell() {}
virtual action_result resolve(expr const & pr) const { virtual action_result resolve(expr const & pr) const override {
try { try {
state & s = curr_state(); state & s = curr_state();
app_builder & b = get_app_builder(); app_builder & b = get_app_builder();