Open
Description
> Datatype`rcd = <| fld : 'a -> bool |>`;
<<HOL message: Defined type: "rcd">>
val it = (): unit
> ``!(x::r.fld). P x``;
<<HOL message: inventing new type variable names: 'a>>
val it = “∀x::r.fld. P x”: term
The printer should invert the parser here; without parentheses around the r.fld
, the parser will fail to parse back the output.