Polymorphism typos and minor nits

[lovettchris]

occaisionally => occasionally

head! is used with no earlier explanation of what the ! means. I think it would be helpful to add a reminder after this paragraph that in Lean "?", "!" are not special operators, they are simply part of the name of a method, leans allows these special characters to be used as part of an identifier. Therefore it is really only a "naming convention" that ? means Optional and "!" means "undo the optional part if you can". I found this very confusing coming from C# where "?" is an actual operator meaning the type to the left is now nullable, until Leo explained it to me.

Prod could mention C# Tuple<T,Q,...>

Sum could mention C "unions"

Sum inl - Leo told me it means "insert left" and "insert right", but I might have misheard...

Sum section doesn't show how to make a Sum value and should add there is no syntactic sugar for making such values.

Unit ==> For instance, a List Unit does not contain anything interesting, but it can express how many entries are expected, and they can be inserted later.

Can you say more about this? I don't get it...

==> Additionally, a function that takes Unit as an argument is a way to express a block of code that can be executed on-demand.

Can you say more about this? I don't get this either?

Empty ==> with a value at type Empty. => You've used this "at type" language a couple times, I keep wanting to read it "of type...". What does "at type" mean?

Naming: Sums, Products, and Units ==> very helpful, thanks!

Messages you may meet ==> "For now, try making the type an argument to the inductive type as a whole, rather than to the constructor."

I tried it:

inductive MyType (α : Type) : Type where
  | ctor : α → MyType

but it also produces an error:

  type expected
  failed to synthesize instance
    CoeSort (Type → Type) ?m.99

Message you may meet ==> "For technical reasons, allowing these datatypes could make it possible to undermine Lean's use as a logic."

What does "use as a logic" mean? How about saying "Lean currently does not allow this for technical reasons."

Exercise on zip, I made the jump in pattern matching that it can handle multiple arguments to figure this out, but probably because I've read lots of Lean code by now. Now sure real noobs will figure that out, this is covered in the next section under Pattern-Matching Definitions, so perhaps this exercise should be moved to 1.7?

match xs, ys with 
| [], b => []
| b, [] => []
| a :: t, b :: u => (a, b) :: zip t u  

and if we mention pattern matching is order sensitive then one can write the more compact version Lean has:

def zip {α β : Type} (xs : List α) (ys : List β) : List (α × β) :=
  match xs, ys with 
  | a :: t, b :: u => (a, b) :: zip t u  
  | _, _ => []

I needed some help with this one:

• Write a function that shows how 2 × x = x + x. It should have type Bool × α → α ⊕ α.

What is the Bool here? You have not yet discussed how a proof is really just a special kind of def that operates on propositions, but I assume that's not what you are asking here, even though the language leads me down that path...?