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

feat(frontends/lean): return the operator associated with constant expressions that are names of builtin values

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-11-13 16:08:21 -08:00
parent 3dea7ae0d6
commit eacd60de9c
1 changed files with 10 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/frontends/lean/frontend.cpp
View file

@ -396,7 +396,16 @@ void frontend::add_mixfixo(unsigned sz, name const * opns, unsigned p, expr cons
to_ext(m_env).add_op(mixfixo(sz, opns, p), d, true, m_env, m_state);
}
operator_info frontend::find_op_for(expr const & n, bool unicode) const {
return to_ext(m_env).find_op_for(n, unicode);
operator_info r = to_ext(m_env).find_op_for(n, unicode);
if (r || !is_constant(n)) {
return r;
} else {
object const & obj = find_object(const_name(n));
if (obj && obj.is_builtin() && obj.get_name() == n)
return to_ext(m_env).find_op_for(obj.get_value(), unicode);
else
return r;
}
}
operator_info frontend::find_nud(name const & n) const {
return to_ext(m_env).find_nud(n);