On 29/09/2021 11:43, Florian Haftmann wrote:
>> * ML antiquotations for type constructors and term constants:
>>
>> \<^Type>‹c›
>> \<^Type>‹c T …› ― ‹same with type arguments›
>> \<^Type>_fn‹c T …› ― ‹fn abstraction, failure via exception TYPE›
>> \<^Const>‹c›
>> \<^Const>‹c T …› ― ‹same with type arguments›
>> \<^Const>‹c for t …› ― ‹same with term arguments›
>> \<^Const_>‹c …› ― ‹same for patterns: case, let, fn›
>> \<^Const>_fn‹c T …› ― ‹fn abstraction, failure via exception TERM›
>
> Excellent!
>
> The abstraction form syntax is not so trivial to grasp, maybe one
> example coulde be added to the NEWS, e. g.
>
> val dest_add_nat = \<^Const_fn>‹Groups.plus \<^Type>‹nat› for a b =>
> ‹(a, b)››
In Isabelle/b9331caf92c3, I have updated the above examples using
Type_fn/Const_fn (they were from an earlier stage, before these extra
antiquotations).
Also note that in Isabelle/e585e5a906ba, I have tune the syntax to allow the
\<^Type>‹nat› in your example stand on its own, without an extra cartouche
around it.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
