why do inductive functions have to return prop

Stream: new members

[Huỳnh Trần Khanh]

they can't return anything else, can they? i guess inductive functions are used to define deduction rules for a particular system, e.g. the MIU system (derivable predicate) or the data.list.perm predicate

[Horatiu Cheval]

You can give inductive definitions into any sort. So, Prop, Type 0, Type 1 and so on. There is nothing restricting them to Prop.
For example docs#nat, the definition of natural numbers lives in Type.

[Horatiu Cheval]

I wouldn't say that you "inductively define functions" but rather that you "inductively define types". Propositions are a particular example of types so the Prop case falls into this. In some cases people refer to inductively defined propositions as "inductive predicates" but it's really the same notion.

[Horatiu Cheval]

What is MIU?

[Huỳnh Trần Khanh]

https://github.com/leanprover-community/mathlib/tree/master/archive/miu_language

[Eric Rodriguez]

structures and classes are essentially inductive functions with syntax sugar

[Eric Rodriguez]

MIU is the formal system used in Gödel Escher Bach @Horatiu Cheval

[Horatiu Cheval]

And it's indeed a good way of thinking them as rules of deduction, or as rules of constructions. inductive basically says "everything that can be constructed, or derived if you prefer, from these rules and these rules only"

[Eric Wieser]

"inductive functions" isn't the normal terminology for the inductive keyword in lean, is it?

[Kevin Buzzard]

(deleted)

[Horatiu Cheval]

Right, it's "inductive type" and the like, predicate, family etc. Inductive function would be misleading in my opinion since functions are not something inductive.