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

chore(frontends/lean/inductive_cmd): add auxiliary assertion for debugging

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-29 22:23:27 -07:00
parent 543fdf840e
commit 231039ad26
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/inductive_cmd.cpp
View file

@ -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);
}