§ Inductive types

§ Coq

§ Expressive Power

T
| .. U (T) 

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

§ Computational content

§ Lean

§ Expressive Power

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

§ Computational content