Prohibitively long elaboration times for inductive types with many constructors

[cpehle]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Elaboration of simple inductive datatypes with >200 constructors takes a long time, this is a problem if one wants to generate code for C++ enums (libclang in this example).

Steps to Reproduce

Invoke lean out.lean --profile --c=out.c on the supplied file.

Expected behavior: Elaboration finishes in a reasonable amount of time.

Actual behavior:

elaboration took 1.07e+03s
out.lean:1:0: error: (deterministic) timeout at 'whnf', maximum number of heartbeats (50000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)
cumulative profiling times:
	elaboration 1.07e+03s
	import 15.1ms
	initialization 15.2ms
	interpretation 0.878ms
	parsing 2.21ms

out.lean.zip

Reproduces how often: 100%

[leodemoura]

The commit above adds the command enum for declaring big enumeration types.
See example in the commit.