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

fix(library/blast/hypothesis): hypotheses are initially inactive

Browse source
This commit is contained in:
Leonardo de Moura 2015-10-06 13:02:06 -07:00
parent e4f0f6a9b4
commit 5d3ed8a634
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/blast/hypothesis.h
View file

@ -31,7 +31,7 @@ class hypothesis {
expr m_value; // justification for this object. expr m_value; // justification for this object.
// Remark: if blast::is_local(m_value) is true, then the hypothesis is an assumption // Remark: if blast::is_local(m_value) is true, then the hypothesis is an assumption
public: public:
hypothesis():m_active(true), m_depth(0) {} hypothesis():m_active(false), m_depth(0) {}
name const & get_name() const { return m_name; } name const & get_name() const { return m_name; }
bool is_active() const { return m_active; } bool is_active() const { return m_active; }
unsigned get_depth() const { return m_depth; } unsigned get_depth() const { return m_depth; }