Email Gateway (Aug 22 2022 at 18:42): Email Gateway (Aug 22 2022 at 18:42):From: Peter Lammich <lammich@in.tum.de>
Hi, consider the following definition
definition finite_rel :: "_ rel ⇒ bool" where "finite_rel ≡ finite"
I would expect to define a constant that is restricted to relations,
i.e., ('a*'a) set, as suggested by
type_synonym 'a rel = "('a × 'a) set"
However, the expansion of type_synonym seems to take place before
expansion of underscores, such that I actually get
consts
finite_rel :: "('a × 'b) set ⇒ bool"
i.e., a constant that is more general than expected.
Is this just a random feature, or is their some rationale behind?
Email Gateway (Aug 22 2022 at 18:42):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Hi Peter,
I'd say that this is a random feature from user perspective, but I
believe that there is some rationale in terms of implementation
complexitz behind that. As you've observed, dummy types are instantiated
with fresh variables only after type abbreviations have been expanded.
The expansion mechanism would have to be more complicated if it had to
track which dummy types variables are derived from the same syntactic
input term.
By the way, IIRC I noticed this behaviour many years ago when we worked
together on our first joint formalisation and you had used dummy types
in there. Since then, I've tried to avoid dummy types unless for
experiments.
Best,
Andreas
Last updated: Apr 19 2024 at 01:05 UTC