Leonardo de Moura 9cc41c4f3d chore(frontends/lean/inductive_cmds): disable broken check ... @kha I have disabled this check. It was implemented 2 years ago by Daniel, and I don't want to fix it. It seems you have already fixed a bug there. AFAICT, this check is just for improving error messages. I believe we may not even need it since the kernel now supports nested inductive types. AFAIR, Daniel implemented this check here because the inductive compiler was introducing a lot of auxiliary declarations that were making the kernel error messages unreadable.		2019-03-04 11:05:21 -08:00
..
compiler	test(tests/compiler/array_test): basic array test	2019-02-16 16:08:49 -08:00
ir	refactor(library/system/io): move into init	2018-08-21 08:43:09 -07:00
lean	chore(frontends/lean/inductive_cmds): disable broken check	2019-03-04 11:05:21 -08:00
playground	test(tests/playground/deriv): Haskell version	2019-02-28 14:57:57 +01:00