max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(kernel/instantiate): add helper function

Browse source
This commit is contained in:
Leonardo de Moura 2016-08-14 16:16:03 -07:00
parent f8e5753a13
commit b6472d043e
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/kernel/instantiate.h
View file

@ -20,6 +20,9 @@ expr instantiate(expr const & e, expr const & s);
/** \brief Replace the free variables with indices 0, ..., n-1 with s[n-1], ..., s[0] in e. */
expr instantiate_rev(expr const & e, unsigned n, expr const * s);
inline expr instantiate_rev(expr const & e, buffer<expr> const & s) {
return instantiate_rev(e, s.size(), s.data());
}
expr apply_beta(expr f, unsigned num_args, expr const * args);
bool is_head_beta(expr const & t);