Questions tagged [coinductive-type]

Use with coinductive types.

1 question with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
11 votes
0 answers

Rules for mutual inductive/coinductive types

Some proof assistants, like Agda and maybe Coq, allow families of mutually defined types, or nested definitions of types, in which some are inductive and others are coinductive. I have no idea what ...
user avatar
  • 2,109