From 231039ad2684b1ef811fa0f6a4fb6162b939e1ff Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 29 Aug 2014 22:23:27 -0700 Subject: [PATCH] chore(frontends/lean/inductive_cmd): add auxiliary assertion for debugging Signed-off-by: Leonardo de Moura --- src/frontends/lean/inductive_cmd.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp index b428db4e3..c97268adb 100644 --- a/src/frontends/lean/inductive_cmd.cpp +++ b/src/frontends/lean/inductive_cmd.cpp @@ -304,6 +304,8 @@ struct inductive_cmd_fn { level_param_names d_lvls; std::tie(d_type, d_lvls) = elaborate_inductive_type(d_type); if (!m_first) { + lean_assert(first_d_type); + lean_assert(first_d_lvls); check_params(d_type, *first_d_type); check_levels(d_lvls, *first_d_lvls); }