Questions tagged [coinductive-type]
Use with coinductive types.
6
questions
11
votes
0
answers
76
views
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 ...
- 2,079
10
votes
1
answer
212
views
Is induction over mutually inductive coinductive types possible?
You can encode ordinals in Coq as
Inductive ord := O | S (n: ord) | Lim (s: nat -> ord).
Suppose you use the following encoding instead
...
- 1,721
9
votes
2
answers
187
views
Comparison between proof assistants for coinductive structures and proofs
I have a quite vague and naïve question: what are the differences between the different proof assistants regarding coinduction?
My motivation is that I'd like to formalize some proofs, basically about ...
- 91
16
votes
1
answer
229
views
What is the state of coinductive types and reasoning in Coq?
Ever since the work by Gimenez for his PhD thesis, Coq has supported positive coinductive types. For example, the type of always-infinite streams containing elements of type ...
- 165
7
votes
1
answer
97
views
Is it possible to define `fib` coinductive stream w/o sized types?
In Agda with --guardedness, we can define productive definitions using copatterns like the following
...
- 4,136
18
votes
1
answer
135
views
When to use coinductive types?
One could define streams in the following manner
...