# Zulip Chat Archive

## Stream: new members

### Topic: What does `?M_1 xyz` mean?

#### Rajiv (Dec 04 2020 at 14:34):

I am new to lean and when working on this section, https://leanprover.github.io/theorem_proving_in_lean/inductive_types.html#enumerated-types and in the following snippet, when I do `#check weekday.rec`

and `#check weekday.rec_on`

, I see something like `?M_1 weekday.sunday`

and `?M_1 n`

.

What does the form `?M_1 xyz`

mean in a type signature?

```
inductive weekday : Type
| sunday : weekday
| monday : weekday
| tuessday : weekday
| wednesday : weekday
| thursday : weekday
| friday : weekday
| saturday : weekday
#check weekday.rec
#check weekday.rec_on
```

#### Kevin Buzzard (Dec 04 2020 at 14:35):

I agree this is confusing. Try `#check @weekday.rec`

#### Rajiv (Dec 04 2020 at 14:37):

Thanks a lot. That helps! :-)

#### Kevin Buzzard (Dec 04 2020 at 14:37):

"For all functions C from `weekday`

to types, if you have a term of type `C sunday`

and a term of type `C monday`

and ... and a term of type `C saturday`

, then I can give you a function which takes any weekday `n`

, and returns a term of type `C n`

"

#### Rajiv (Dec 05 2020 at 06:21):

Are there more examples of how to read `Π`

type signatures somewhere? I am finding this way of reading type signatures quite useful.

#### Kevin Buzzard (Dec 05 2020 at 14:13):

I tried to read recursors when I was getting the hang of this stuff. For me when I was learning, I found it helpful to just focus on the idea that there were only two universes, `Prop`

(the universe of types which represent true/false statements like 2+2=4 and 2+2+5) and `Type`

(the universe of types which represent collections of stuff, like the real numbers). (This idea isn't actually true, there are infinitely many type universes because Type has to have a type, but this is just a quirk of the theory). When I see `Sort u`

I would interpret it as meaning "Either `Prop`

or `Type`

". With that in mind, here is `nat.rec`

(which is quite a difficult one):

```
nat.rec : Π {C : ℕ → Sort u}, C 0 → (Π (d : ℕ), C d → C d.succ) → Π (n : ℕ), C n
```

If we interpret `Sort u`

as `Prop`

, this says the principle of mathematical induction, namely that for all families `C 0, C 1, C 2, ...`

of true-false statements, if we know `C 0`

is true and if we know that for all d, `C d`

implies `C (d + 1)`

(note that `d.succ`

just means `d + 1`

), then we can conclude that for all n, `C n`

is true.

If on the other hand we interpret `Sort u`

as `Type`

, then this says the principle of mathematical recursion, namely that for all families `C 0`

, `C 1`

, ... `C n`

, ... of types or sets or however you want to think of them, if we have an element of `C 0`

, and if we also have a method which given `d`

and an element of `C d`

produces an element of `C (d + 1)`

, then we have a method to produce an element of `C n`

for all `n`

.

#### Rajiv (Dec 05 2020 at 15:06):

Thanks again Prof. Kevin. I really appreciate your reply and pointers.

Last updated: Dec 20 2023 at 11:08 UTC