Errata for The Little Typer

Return to the main page.
38 In The Initial Second Commandment of λ, the name f should have been written in a serif italic font, like so: f.
77 Frame 30 implies that rec-Nat is strictly more powerful than iter-Nat, while it is in fact possible to derive rec-Nat from iter-Nat using a pair for the base. Felix Herrmann and Carl Howells
93 In frame 1, the reference to frame 2:70 should have been a reference to frame 2:80. Vassili Bykov
124 In frame 61, the definition of concat is incorrect. It reverses its second argument. Alex Brown and Stuart A. Kurtz
157 In the right hand side of frame 53, (mot-last ℓ-1) should read (mot-last E ℓ-1). Graydon Hoare
157 In the right hand side of frame 55, step 5 in the same-as chart is missing a step number, and step 6 is numbered 5. Graydon Hoare
161 In frame 68, the reference to frame 66 should instead be a reference to frame 67.
358 The type of base is incorrect. It should instead be
(Π ((k Nat))
  (mot zero (add1 k) (zero-smallest k)))
David Moews