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

Makarius makarius at sketis.net
Thu Oct 14 10:06:28 CEST 2021

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,

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

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


More information about the isabelle-dev mailing list