It is an essential feature of proof assistants such as Agda and Coq that it enables users to define their own inductive types and families by listing their introduction rules (the types of their constructors). This is much like in typed functional programming languages such as Haskell and the different dialects of ML. However, unlike in these programming languages the schema for inductive definitions in intuitionistic type theory enforces a restriction amounting to well-foundedness of the elements of the defined types.