Description of `mkFreshExprMVar` with `type?` = `none` in chapter "MetaM" is incorrect

[whxvd]

Thanks a lot for this book. It is a great resource for diving into great stuff. I am having a very good time.

The description of mkFreshExprMVar in the "MetaM" chapter seems to incorrectly describe its type? parameter in the case it is none. The book states: "If none, the target type is Sort ?u".

But as far as I understand its definition, mkFreshExprMVar none instead should effectively allow any type as target type, not just sorts. It does that by introducing an additional metavariable as the target type; the target type of that metavariable is Sort ?u.