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: Sep 25 2022 at 23:25 UTC