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

fix(kernel/normalizer): compilation problem with clang++

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-18 08:46:36 -08:00
parent 418623b874
commit 7b2fea3fab
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/kernel/normalizer.cpp
View file

@ -117,7 +117,7 @@ class normalizer::imp {
/** \brief Convert the value \c v back into an expression in a context that contains \c k binders. */
expr reify(expr const & v, unsigned k) {
return replace(v, [&](expr const & e, unsigned DEBUG_CODE(offset)) {
return replace(v, [&](expr const & e, unsigned DEBUG_CODE(offset)) -> expr {
lean_assert(offset == 0);
lean_assert(!is_lambda(e) && !is_pi(e) && !is_metavar(e) && !is_let(e));
if (is_var(e)) {