No effort was put into looking whether coinduction works with the backend.
Currently, all inductives are inserted in the environment with type Finite, and IntoAny for AllowedEliminations.
Those should be properly set if we care about coinductions.
There's a gotcha: Rocq only allows mutually-defined coinductive datatypes. Or mutually-defined inductives. But I don't think a mixture of both is supported. Probably why the RecursivityKind is set at the level of the MutualInductiveBody.
Agda doesn't care about that and freely allows mutually-defined inductive datatypes and coinductive records. We should detect this and throw a hard error, probably.
No effort was put into looking whether coinduction works with the backend.
Currently, all inductives are inserted in the environment with type
Finite, andIntoAnyforAllowedEliminations.Those should be properly set if we care about coinductions.
There's a gotcha: Rocq only allows mutually-defined coinductive datatypes. Or mutually-defined inductives. But I don't think a mixture of both is supported. Probably why the
RecursivityKindis set at the level of theMutualInductiveBody.Agda doesn't care about that and freely allows mutually-defined inductive datatypes and coinductive records. We should detect this and throw a hard error, probably.