Email Gateway (Aug 18 2022 at 17:55): Email Gateway (Aug 18 2022 at 17:55):From: Mathieu Giorgino <mathieu.giorgino@irit.fr>
It does not work for any datatype (for example as soon as a non-countable type
is used in the datatype) but it could be integrated in the datatype package
with some checks.
However, I don't know if the time penalty (which isn't so big but there
anyway) on a so much used feature worth the benefit... unless it would be
present as an option (perhaps even with a recursive call on included non-
instantiated types). And an option would be mostly equivalent to (in fact even
less flexible than) a new command or an ML call subsequent to the datatype
definition.
Mathieu
Le jeudi 21 juillet 2011 19:02:41 Peter Lammich a écrit :
Last updated: Nov 21 2024 at 12:39 UTC