[isabelle-dev] NEWS: ML antiquotations for type constructors and term constants

[Makarius]

On 14.10.21 09:49, Peter Lammich wrote:
> 
> I'm also, in many cases, in favour of clear and readable code over
> efficient and less readable. (That's the reason why we use functional
> programming for Isabelle, in first place!)

The new \<^Type> / \<^Const> antiquotations are designed to be both
efficient in the runtime, and efficient in the source text (readable,
maintainable).

As usual, it is just a matter to get used to a new way of thinking,
which is actually closer to the old way of direct use of datatype
constructors.

Moreover, the treatment of type arguments is much more concise: the term
(patterns) are rather awkward in that respect: both in the text and at
runtime (fastype_of).


This thread was mainly meant to figure out shortcomings that can be
improved further: this often becomes apparent in concrete use, e.g.
while converting an application to the new format.

(Doing that here and there, I did already see another are of reform,
namely "instantiate" forms for thm, cterm, maybe even term.)


	Makarius