4
votes
2answers
121 views

Define a special verbatim commmand

To learn more about Plain TeX, I try to define a special verbatim command \verb{code}, which puts code inside braces. When there is no braces in code, It's easy. But when there are some balanced ...
1
vote
0answers
157 views

Using braces in verbatim environment

I want to put some code in a verbatim environment: \begin{verbatim} data _≥_ : Nat → Nat → Set where ge0 : {y : Nat} → y ≥ zero geS : {x : Nat} {y : Nat} → x ≥ y → suc x ≥ ...
2
votes
1answer
116 views

too many curly brace using verbdef

I would like to create an inline verbatim text for a regular expression. The verbdef package does not like when I put curly braces into its second argument. I tried with escaping backslashes but that ...
4
votes
1answer
203 views

The command \string does not print curly braces of its argument

While printing the List of Symbols, I would like, in a draft, to print the definition commands as well. For instance, consider the following commands: \providecommand{\perm}{\ensuremath{\pi}} ...