HOL icon indicating copy to clipboard operation
HOL copied to clipboard

Restricted quantifier pretty-printing failure

Open mn200 opened this issue 7 years ago • 0 comments

> 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.

mn200 avatar May 01 '18 03:05 mn200