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: Apr 19 2024 at 20:15 UTC