Questions tagged [inductive-type]
In terms of categorical semantics, an inductive type is a type whose interpretation is given by an initial algebra of an endofunctor. (from nLab)
6
questions
12
votes
1
answer
490
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
...
- 2,868
4
votes
1
answer
228
views
Making a finite graph type in Lean - introduction rule
I'm making a finite directed graph type in Lean. I know type theory from an abstract point of view, but I'm struggling to find the way Lean would produce a type playing the role of a "finite set&...
18
votes
1
answer
1k
views
What are the complex induction patterns supported by Agda?
A question was recently asked on the Coq-club mailing list on Coq rejecting a nastily nested inductive type. We encountered a similar difficulty while trying to port code from Agda to Coq: Agda ...
- 5,510
10
votes
2
answers
547
views
Replacing (strict) positivity with monotonicity on propositions
When defining an inductive type, there is a famous "positivity" restriction on the constructor types. For example, an inductive type $\mathsf D$ has constructor $\mathsf c : F(\mathsf D) \to ...
- 4,025
9
votes
2
answers
822
views
Construction of inductive types "the hard way"
Most theorem provers simply axiomize inductive types (or equivalently W types) in the abstract which is fine.
But I'm curious about explicit constructions of inductive types within the theory.
I ...
- 2,868
1
vote
0
answers
179
views
Descriptions of heterogenous datatypes
When attempting to describe the datatype as appearing in my previous question, using indexed descriptions in style of The Gentle Art of Levitation to describe this datatype (using Agda for examples):
<...
- 547