diff --git a/src/frontends/lean/pp.h b/src/frontends/lean/pp.h index e3a70b0b31..ecb549ad98 100644 --- a/src/frontends/lean/pp.h +++ b/src/frontends/lean/pp.h @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once +#include #include #include #include "util/pair.h" diff --git a/src/frontends/lean/scanner.cpp b/src/frontends/lean/scanner.cpp index c63446f849..402d72cdfc 100644 --- a/src/frontends/lean/scanner.cpp +++ b/src/frontends/lean/scanner.cpp @@ -160,7 +160,7 @@ auto scanner::read_quoted_symbol() -> token_kind { } else if (c != '\"' && c != '\n' && c != '\t') { m_buffer += c; } else { - // TODO: intra-token space + // TODO(Leo): intra-token space throw_exception("invalid quoted symbol, invalid character"); } }