Add set_option pp.explicit false in Weak Head Normal Form example

[kpadmasola]

In the following example in Weak Head Normalisation section:

the expected output is:

#eval whnf' `(List.cons 1 [])
-- [1]

but the actual output is:

#eval whnf' `(List.cons 1 [])
-- @List.cons Nat 1 (@List.nil Nat)

This PR fixes the example code so that the actual output matches the one in the book.

[kpadmasola]

@Julian Can you please review ? Thanks!

[Julian]

I think the real issue here is above on line 569, and specifically that that line should have been doing

set_option pp.explicit true in

(with the in) rather than globally changing the setting?

Could you perhaps try that instead and check whether that makes everything look correct?

Meanwhile, as someone who doesn't know much at all about metaprogramming, I find this example confusing to start off with -- the text just got finished explaining what the general form of something in WHNF is, and then here immediately starts with an example that prints differently? Naively to me it definitely seems worthwhile to explain that the pretty printer can make something look not WHNF even when it is, but starting with such an example seems weird if I follow what the text is saying.

But it does seem like the intention is to show [1] and that that's what it used to do before the change to 569, so I'm happy to merge if you take a look at the in bit above?

And thanks as usual!

[kpadmasola]

@Julian The change you suggested worked, thanks! PR updated.