§ Inductive types

§ Coq

§ Expressive Power

• Bare Inductives
• Nested inductives: The constructor of the nesting cannot be a mutual [So we can have T := ... List T, but not T := ... Mutual1 T where Mutual1T := Mutual2 T and Mutual2 T := Mutual1 T]
• Mutual inductives: All parameters of inductives in the mutual group must be the same.
• Nested Mutual inductives: Not supported, something like:

T
| .. U (T)

U
| .. T

does not work due to the presence of U(T).

§ Computational content

• Bare inductives: primitive recursion principle fix, kernel has support for fix reduction (iota)
• Nested inductives: primitive recursion principle using fix and match. Kernel has support for fix reduction, and match is also known by the kernel.
• Mutual inductives: generates 'simple' recursion principles for each element of the mutual.
• Need to use the scheme command to get the full recursion principle.
• Primitive recursion principle using fix and match.

§ Lean

§ Expressive Power

• Bare inductives
• Nested inductives: works perfectly!

mutual
inductive U1 (S: Type): Type :=
| mk: U2 S → U1 S
| inhabitant: U1 S

inductive U2 (S: Type): Type :=
| mk: U1 S → U2 S
| inhabitant: U2 S
end

inductive T
| mk: U1 T → T

• Mutual inductives: All parameters of inductives types in the mutual group must be the same.

§ Computational content