§ 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