Explore our questions

5 votes
2 answers
116 views

Comparing indexed induction to recursion

1 vote
0 answers
57 views

Heterogeneous lists, large indices

1 vote
0 answers
43 views

how to inductively define paths from paths using unimath

1 vote
1 answer
89 views

How to apply constructor injectivity in the goal

0 votes
1 answer
153 views

Why inductive types (or variants) are so rigid in terms of the set of constructors

2 votes
2 answers
208 views

How to reason about and extract code for inductive types with negative occurrences in Coq?

1 vote
0 answers
46 views

Can you always replace mutually recursive references with parameters?

1 vote
0 answers
57 views

Why does Coq not allow constructor argument types to be strictly positive mutual inductive types?

4 votes
1 answer
175 views

Co-induction principle

2 votes
1 answer
162 views

Induction scheme on two arguments for custom type in Coq

15 votes
1 answer
1k views

What are the complex induction patterns supported by Agda?

-2 votes
2 answers
103 views

Help with strong induction

6 votes
4 answers
750 views

Inductive vs. recursive definitions

9 votes
2 answers
805 views

Construction of inductive types "the hard way"

Browse more Questions