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

chore(inductive_compiler/mutual): better error message for non-positive occurrences

Browse source
This commit is contained in:
Daniel Selsam 2016-10-04 20:25:38 -07:00 • committed by Leonardo de Moura
parent 3d2ff8a76d
commit 6b8583ecac
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/library/inductive_compiler/mutual.cpp
View file

@ -206,6 +206,9 @@ class add_mutual_inductive_decl_fn {
expr ty = m_tctx.whnf(arg_type);
buffer<expr> locals;
while (is_pi(ty)) {
if (translate_ind_app(binding_domain(ty))) {
throw exception(sstream() << "invalid mutually inductive type, non-positive occurrence in introduction rule: " << arg_type);
}
expr l = mk_local_for(ty);
locals.push_back(l);
ty = instantiate(binding_body(ty), l);