The Coq mailing list

[Guillaume Claret <guillaume AT claret.me>]

Hi,

The idea of going to the integers sounds nice!

In order to deal with smaller inductives, I wonder if you could 
factorize your inductives to have smaller ones, without breaking all the 
existing developments. Using one category for assignments, one category 
for bindings, ...

Cheers,
Guillaume Claret

Le 17/06/2020 à 16:12, Sylvain Boulmé a écrit :
> Hi Alan,
>
> I wonder whether you could deduce your eq_dec equality from an injection 
> to positive or Z integers (see the file in attachment).
>
> I guess that proving "id" hypothesis would not blow up on your example.
>
> Sylvain.
>
> Le 17/06/2020 à 15:44, Alan Schmitt a écrit :
> > Hello,
> >
> > As part of a larger project, I'm generating a big inductive type for
> > which I need to prove decidable equality. Running ~coqc js.v~ on the
> > attached file result in a Stack Overflow. I tried duplicating the line
> > where the problem occurs (instead of using "all:"), but I then run out
> > of memory and coqc is killed.
> >
> > I feel like I'm not using the correct approach. Do you have suggestions
> > on how to deal with this?
> >
> > Thanks,
> >
> > Alan