I found two typos in the MetaM chapter of the online version of the book:
In the first example using Eq.trans, the sentence "Now the third apply comes in. Since ?b has been assigned, the target of ?m3 is now f (f a) = a", ?m3 is actually f a = a at this point.
2.In the sentence "See the Metavariable Kinds section (but the default is usually correct)." the link doesn't exist. There doesn't seem to be a section on metavariable kinds.
I found two typos in the
MetaMchapter of the online version of the book:Eq.trans, the sentence "Now the third apply comes in. Since?bhas been assigned, the target of?m3is nowf (f a) = a",?m3is actuallyf a = aat this point. 2.In the sentence "See the Metavariable Kinds section (but the default is usually correct)." the link doesn't exist. There doesn't seem to be a section on metavariable kinds.