The Coq mailing list

[Petar Maksimovic <petar.maksimovic AT gmail.com>]

Thanks Cedric and Gregory,

I'll give it a go with the modular approach, it should be sufficiently fast.

400+ constructors are needed because it's the full operational
semantics (in pretty-big-step) of ES5 Javascript expressions (see
https://github.com/jscert/jscert/blob/master/coq/JsPrettyRules.v). I
doubt that it can be refactored into multiple inductives at this point
in the development.

On a side note, is there a way, when doing Check ________,  of
instructing Coq to print the statement fully, without putting two dots
(..) in places where it estimates the printout would be too large or
poorly formatted?

Cheers,
Petar

On 9 September 2015 at 13:55, Cedric Auger 
<sedrikov AT gmail.com>
 wrote:
>
>
> 2015-09-09 13:52 GMT+02:00 Cedric Auger 
> <sedrikov AT gmail.com>:
>>
>>
>>
>> 2015-09-08 21:44 GMT+02:00 Gregory Malecha 
>> <gmalecha AT cs.harvard.edu>:
>>>
>>> You might be able to do something with computation, but it depends on
>>> your exact of [inversion]. If you were doing equalities then you might be
>>> able to write a lemma like:
>>>
>>> Lemma inv_my_type_eq : forall a b : my_type,
>>>   a = b ->
>>>   match a , b with
>>>   | ... , ... => ....
>>>   end.
>>
>>
>> I would advise to be more careful if you have 400+ constructors. This kind
>> of pattern matching expands to 1600+ cases, and is not especially wishable.
>
>
> I meant 160,000
>
> cases.