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

[Makarius]

On 14/10/2021 10:22, Peter Lammich wrote:
> 
> The usage of mk_term/pat, and the fact that it has been invented at
> least twice independently, indicates that there is some sweet spot
> here, which, at least for some use cases, allows a very concise
> notation.

All these attempts are rather fragile and incomplete. Over a long time, I used
to tell the story myself, that we should use inner syntax for term patterns
and it never quite worked out.

There are various dimensions in the problem that should not be collapsed:

  * Patterns should be considered separately from expressions (but: the new
\<^Type>/\<^Const> antiquotations are so elementary and close to ML that they
can do both).

  * Expressions can be easily used with concrete syntax, e.g. a version of
@{term} / @{cterm} / @{thm} combined with instantiation (Thm.instantiate): I
have started to think about that some weeks ago, and might manage to do
something for the release. This will supersede earlier attempts like @{mk_term}.

  * Genuine cterms are probably better treated like the core logic does, e.g.
with Thm.match / Thm.first_order_match. Instead of raw decomposition of cterms
(with awkward invention of frees for bounds), regular matching can treat
binders directly.


	Makarius