1
vote
0answers
69 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
103 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
194 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}} ...