Email Gateway (Aug 18 2022 at 15:14): Email Gateway (Aug 18 2022 at 15:14):From: Christian Sternagel <christian.sternagel@uibk.ac.at>
Hi there,
is there a mode (for document antiquotations) such that plain ASCII
symbols are used. If yes, what is it's name?
More specifically, I would like to get
datatype 'a * 'b = Pair 'a 'b
as the result of
@{datatype[mode=...] "*"}
Is this possible?
cheers
chris
Last updated: Apr 25 2024 at 04:18 UTC