In Section 6.2 (Type inference by example) on p. 117, id and idfun are interleavingly used as names of the same function. Only one of them should be used for clarity.
Source code: https://github.com/math-comp/mcb/blob/master/tex/chTypeInference.tex#L171-L230
In Section 6.2 (Type inference by example) on p. 117,
idandidfunare interleavingly used as names of the same function. Only one of them should be used for clarity.Source code: https://github.com/math-comp/mcb/blob/master/tex/chTypeInference.tex#L171-L230