search

UniMath / SymmetryBook

This book will be an undergraduate textbook written in the univalent style, taking advantage of the presence of symmetry in the logic at an early stage.
Creative Commons Attribution Share Alike 4.0 International
397 stars 23 forks source link

\NN macro #102

Closed DanGrayson closed 3 years ago

DanGrayson commented 3 years ago

For some reason $\prod_{n_{\NN}} P_n$ works but $\prod_{n_\NN} P_n$ doesn't. Here is the error message:

! Missing { inserted.
<to be read again> 
                   \@tempcnta 
l.117 ...ion $n \mapsto p_n$ of type $\prod_{n_\NN
                                                  } P_n$, where $P_n$ is the...
DanGrayson commented 3 years ago

Never mind -- I wanted : instead of _.