Thank you both for your explanations: indeed this «
whatever » command in MetaPost is magic and very useful (I am not sure
whether it is a command only in MetaFun, or it exists also in the
original MetaPost).
You have to go further back, whatever already existed in MetaFont.