Content deleted Content added
m Protected "Induction-recursion": Persistent disruptive editing: IP-jumping edit warrior ([Edit=Require autoconfirmed or confirmed access] (expires 13:27, 13 May 2018 (UTC)) [Move=Require autoconfirmed or confirmed access]... |
m Padlock |
||
Line 1:
{{pp-semi|small=yes}}
In [[intuitionistic type theory]] (ITT), a discipline within [[mathematical logic]], '''induction-recursion''' is a feature for simultaneously declaring a type and function on that type. It allows the creation of larger types, such as universes, than [[Intuitionistic type theory#Inductive types|inductive types]]. The types created still remain [[Predicativity|predicative]] inside ITT.
| |||