Florian Haftmann wrote:
> Since this is part of the syntax layer,
>
> val unit = (fn Const (@{const_syntax Product_Type.Unity},__) => true |
> _ => false);
>
> is the appropriate antiquotation.
Thanks.
It's not entirely satisfying (I was hoping I could get away with not
mentioning Produc
The pretty printing in the record package is currently broken.
Things like term "(| x = 0 |)" get printed as "(| x = 0, ... = () |)", i.e.
the "more" component is not suppressed when it should.
It all comes down to the line
val unit = (fn Const ("Unity",_) => true | _ => false);
in HOL/Too
On Wed, 13 Feb 2008, Gerwin Klein wrote:
> What does work is replacing it by "\\<^const>Product_Type.Unity", but
> that feels very ad-hoc to me (I'm not sure where the \<^const> comes
> from), so I haven't committed it yet.
The SML antiquotation @{const_syntax Unity} should do the trick.
>> val unit = (fn Const (@{const_syntax Product_Type.Unity},__) => true |
>> _ => false);
>
> It's not entirely satisfying (I was hoping I could get away with not
> mentioning Product_Type), but better than what I had before. I'll commit
> this then.
Indeed, the Product_Type is not necess
> It all comes down to the line
>
> val unit = (fn Const ("Unity",_) => true | _ => false);
>
> in HOL/Tools/record_package.ML which doesn't match Unity correctly.
>
> Unfortunately, replacing it by @{term "Unity} or @[term "()"} doesn't work.
Since this is part of the syntax layer,
