Numerous edits of a very pedantic nature to the NaturalNumbers example, in the interests of consistency of presentation. Highlighting a couple of points
changed false to False
changed empty to Empty
changed intros to intro (I recall a discussion on Zulip where the general opinion seemed to be that intro should be used in preference to intros and that perhaps intros should be dropped from Lean 4).
Numerous edits of a very pedantic nature to the NaturalNumbers example, in the interests of consistency of presentation. Highlighting a couple of points
falsetoFalseemptytoEmptyintrostointro(I recall a discussion on Zulip where the general opinion seemed to be thatintroshould be used in preference tointrosand that perhapsintrosshould be dropped from Lean 4).