michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
lean2/src/library
History
Leonardo de Moura f80106a895 chore(*): use 'explicit operator bool' everywhere. 
operator bool() may produce unwanted conversions.
For example, we had the following bug in the code base.

...
   object const & obj = find_object(const_name(n));
   if (obj && obj.is_builtin() && obj.get_name() == n)
...

obj.get_name() has type lean::name
n              has type lean::expr

Both have 'operator bool()', then the compiler uses the operator to
convert them to Boolean, and then compare the result.
Of course, this is not our intention.

After this commit, the compiler correctly signs the error.
The correct code is

...
   object const & obj = find_object(const_name(n));
   if (obj && obj.is_builtin() && obj.get_name() == const_name(n))
...

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-02 23:02:45 -08:00
..
all feat(library/hidden_defs): hidden definitions are just hints for tactics and solvers 2013-12-01 10:27:27 -08:00
arith feat(library/hidden_defs): hidden definitions are just hints for tactics and solvers 2013-12-01 10:27:27 -08:00
cast feat(kernel/environment): track which modules were already imported 2013-11-17 18:15:44 -08:00
elaborator feat(library/elaborator): modify how elaborator handles constraints of the form ?M << P and P << ?M, where P is a proposition. 2013-11-29 09:15:01 -08:00
rewriter fix(library/rewriter): use Abst axiom in lambda_body RW 2013-12-01 22:24:12 -05:00
tactic chore(*): use 'explicit operator bool' everywhere. 2013-12-02 23:02:45 -08:00
basic_thms.cpp feat(library/tactic): add unfold tactic 2013-12-01 08:51:56 -08:00
basic_thms.h feat(library/tactic): add absurd_tactic 2013-12-01 07:55:00 -08:00
CMakeLists.txt feat(library/hidden_defs): hidden definitions are just hints for tactics and solvers 2013-12-01 10:27:27 -08:00
context_to_lambda.cpp Add support for creating unique internal names. 2013-09-24 11:01:30 -07:00
context_to_lambda.h Use fullpath in #include directives. 2013-09-12 20:04:10 -07:00
deep_copy.cpp feat(kernel/expr): add new mk_app template for creating applications using a collection 2013-10-27 08:53:58 -07:00
deep_copy.h Use fullpath in #include directives. 2013-09-12 20:04:10 -07:00
expr_lt.cpp fix(library/expr_lt): fix bug when using hash codes 2013-11-14 13:18:33 -08:00
expr_lt.h feat(expr_lt): improve expr_lt performance by using hash codes, and add more tests 2013-09-25 21:59:58 -07:00
expr_pair.h feat(kernel/expr): add hash code based on allocation time 2013-11-14 02:43:11 -08:00
hidden_defs.cpp feat(library/hidden_defs): hidden definitions are just hints for tactics and solvers 2013-12-01 10:27:27 -08:00
hidden_defs.h feat(library/hidden_defs): hidden definitions are just hints for tactics and solvers 2013-12-01 10:27:27 -08:00
io_state.cpp refactor(bindings/lua): move Lua bindings to the file associated with them 2013-11-26 19:15:56 -08:00
io_state.h refactor(bindings/lua): move Lua bindings to the file associated with them 2013-11-26 19:15:56 -08:00
kernel_bindings.cpp feat(library/hidden_defs): hidden definitions are just hints for tactics and solvers 2013-12-01 10:27:27 -08:00
kernel_bindings.h feat(library/hidden_defs): hidden definitions are just hints for tactics and solvers 2013-12-01 10:27:27 -08:00
max_sharing.cpp feat(kernel): add (optional) field m_type to expr_const, this field is useful for implementing the tactic framework 2013-11-19 11:21:52 -08:00
max_sharing.h Use consistent naming conventions 2013-09-17 14:43:07 -07:00
placeholder.cpp fix(*): typo 2013-12-02 08:46:47 -08:00
placeholder.h fix(*): typo 2013-12-02 08:46:47 -08:00
register_module.h feat(library/hidden_defs): hidden definitions are just hints for tactics and solvers 2013-12-01 10:27:27 -08:00
type_inferer.cpp feat(util): add primitives for checking the amount of available stack space 2013-12-01 17:19:27 -08:00
type_inferer.h refactor(bindings/lua): move Lua bindings to the file associated with them 2013-11-26 19:15:56 -08:00
update_expr.cpp feat(library/tactic): add unfold_tactic() that unfolds every non-hidden definition 2013-12-01 10:41:05 -08:00
update_expr.h feat(library/tactic): add unfold_tactic() that unfolds every non-hidden definition 2013-12-01 10:41:05 -08:00