Stream: Beginner Questions

Topic: typesetting a former definition


view this post on Zulip Gergely Buday (Nov 13 2020 at 08:40):

Is it possible to typeset a former datatype definition that I imported?

I tried

 @{term [display = true] com}

and the typ and type antiquotation, with source/display true, to no avail.

Is this possible with an antiquotation? If not, is there a workaround other then copying the source text again?


Last updated: Aug 13 2022 at 05:18 UTC