On Thu, 2021-10-14 at 10:06 +0200, Makarius wrote: > 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).
but they are clearly less concise than mk_term/pat, at least for some applications. 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. This still has some problems in other cases (e.g., treatment of types). However, this should not be a reason for abandoning this promising find, but to try to understand it further: in what cases is use of mk_term/pat adequate, and in what cases do we have to fall back to the more low-level but robust/general Type/Const. Can we even have both: the benefit of concise treatment of type arguments AND the benefit of concise, high-level notation? -- Peter > > 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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
