Editing Type theory (section)

====Inductive types====
Inductive types are a general template for creating a large variety of types. In fact, all the types described above and more can be defined using the rules of inductive types. Two methods of generating inductive types are [[induction-recursion]] and [[induction-induction]]. A method that only uses lambda terms is [[Mogensen–Scott encoding|Scott encoding]].

Some [[Proof assistant|proof assistants]], such as [[Rocq (software)|Rocq]] (previously known as ''Coq'') and [[Lean (proof assistant)|Lean]], are based on the calculus for inductive constructions, which is a [[calculus of constructions]] with inductive types.