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

feat(kernel): let Pi/Fun also take local constants

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-19 17:03:48 -07:00
parent df9c935f0a
commit 9de8249d8f
2 changed files with 5 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/kernel/abstract.h
View file

@ -39,7 +39,7 @@ inline expr Fun(name const & n, expr const & t, expr const & b, binder_info cons
return mk_lambda(n, t, abstract(b, mk_constant(n)), bi);
}
inline expr Fun(expr const & n, expr const & t, expr const & b, binder_info const & bi = binder_info()) {
return mk_lambda(const_name(n), t, abstract(b, n), bi);
return mk_lambda(named_expr_name(n), t, abstract(b, n), bi);
}
inline expr Fun(std::pair<expr const &, expr const &> const & p, expr const & b) { return Fun(p.first, p.second, b); }
expr Fun(std::initializer_list<std::pair<expr const &, expr const &>> const & l, expr const & b);
@ -55,7 +55,7 @@ inline expr Pi(name const & n, expr const & t, expr const & b, binder_info const
return mk_pi(n, t, abstract(b, mk_constant(n)), bi);
}
inline expr Pi(expr const & n, expr const & t, expr const & b, binder_info const & bi = binder_info()) {
return mk_pi(const_name(n), t, abstract(b, n), bi);
return mk_pi(named_expr_name(n), t, abstract(b, n), bi);
}
inline expr Pi(std::pair<expr const &, expr const &> const & p, expr const & b) { return Pi(p.first, p.second, b); }
expr Pi(std::initializer_list<std::pair<expr const &, expr const &>> const & l, expr const & b);
@ -67,5 +67,5 @@ inline expr Pi(expr const & local, expr const & b) { return Pi(1, &local, b); }
- \brief Create a Let expression (Let x := v in b), the term b is abstracted using abstract(b, x).
-*/
inline expr Let(name const & x, expr const & t, expr const & v, expr const & b) { return mk_let(x, t, v, abstract(b, mk_constant(x))); }
inline expr Let(expr const & x, expr const & t, expr const & v, expr const & b) { return mk_let(const_name(x), t, v, abstract(b, x)); }
inline expr Let(expr const & x, expr const & t, expr const & v, expr const & b) { return mk_let(named_expr_name(x), t, v, abstract(b, x)); }
}

2
src/kernel/expr.h
View file

@ -608,6 +608,8 @@ expr const & get_app_rev_args(expr const & e, buffer<expr> & args);
then return \c e.
*/
expr const & get_app_fn(expr const & e);
/** \brief Return the name of constant, local, metavar */
inline name const & named_expr_name(expr const & e) { return is_constant(e) ? const_name(e) : mlocal_name(e); }
// =======================================