@@ -15,7 +15,7 @@ \section{Basic Usage}\label{basic-usage}}
1515
1616We can use all Idris 2 features. Here's an example code block:
1717
18- \let\KatlaSnippet\relax {}\newcommand \KatlaSnippet [1][]{\UseVerbatim [#1]{KatlaSnippet}}
18+ \let\KatlaSnippet\relax {}\newcommand \KatlaSnippet [1][]{\BUseVerbatim [#1]{KatlaSnippet}}
1919\begin {SaveVerbatim }[commandchars=\\ \{\} ]{KatlaSnippet}
2020\IdrisFunction {x}\KatlaSpace {}\IdrisKeyword {:}\KatlaSpace {}\IdrisType {Nat}\KatlaNewline {}
2121\IdrisFunction {x}\KatlaSpace {}\IdrisKeyword {=}\KatlaSpace {}\IdrisData {1}\KatlaSpace {}\IdrisFunction {+}\KatlaSpace {}\IdrisData {2}\KatlaNewline {}
@@ -26,7 +26,7 @@ \section{Basic Usage}\label{basic-usage}}
2626as to provide alternate definitions for functions. Consider this
2727function signature:
2828
29- \let\KatlaSnippet\relax {}\newcommand \KatlaSnippet [1][]{\UseVerbatim [#1]{KatlaSnippet}}
29+ \let\KatlaSnippet\relax {}\newcommand \KatlaSnippet [1][]{\BUseVerbatim [#1]{KatlaSnippet}}
3030\begin {SaveVerbatim }[commandchars=\\ \{\} ]{KatlaSnippet}
3131\IdrisFunction {f}\KatlaSpace {}\IdrisKeyword {:}\KatlaSpace {}\IdrisType {Vect}\KatlaSpace {}\IdrisBound {n}\KatlaSpace {}\IdrisBound {a}\KatlaSpace {}\IdrisKeyword {\KatlaDash {}>}\KatlaSpace {}\IdrisType {Vect}\KatlaSpace {}\IdrisKeyword {(}\IdrisBound {n}\KatlaSpace {}\IdrisFunction {+}\KatlaSpace {}\IdrisBound {n}\IdrisKeyword {)}\KatlaSpace {}\IdrisBound {a}\KatlaNewline {}
3232\end {SaveVerbatim }
@@ -39,7 +39,7 @@ \section{Basic Usage}\label{basic-usage}}
3939\end {SaveVerbatim }
4040\KatlaSnippet {}:
4141
42- \let\KatlaSnippet\relax {}\newcommand \KatlaSnippet [1][]{\UseVerbatim [#1]{KatlaSnippet}}
42+ \let\KatlaSnippet\relax {}\newcommand \KatlaSnippet [1][]{\BUseVerbatim [#1]{KatlaSnippet}}
4343\begin {SaveVerbatim }[commandchars=\\ \{\} ]{KatlaSnippet}
4444\IdrisFunction {f}\KatlaSpace {}\IdrisBound {xs}\KatlaSpace {}\IdrisKeyword {=}\KatlaSpace {}\IdrisBound {xs}\KatlaSpace {}\IdrisFunction {++}\KatlaSpace {}\IdrisBound {xs}\KatlaNewline {}
4545\end {SaveVerbatim }
@@ -48,7 +48,7 @@ \section{Basic Usage}\label{basic-usage}}
4848By repeating the signature in a different namespace, in a hidden code
4949block, I can give an alternate definition:
5050
51- \let\KatlaSnippet\relax {}\newcommand \KatlaSnippet [1][]{\UseVerbatim [#1]{KatlaSnippet}}
51+ \let\KatlaSnippet\relax {}\newcommand \KatlaSnippet [1][]{\BUseVerbatim [#1]{KatlaSnippet}}
5252\begin {SaveVerbatim }[commandchars=\\ \{\} ]{KatlaSnippet}
5353\IdrisFunction {f}\KatlaSpace {}\IdrisBound {xs}\KatlaSpace {}\IdrisKeyword {=}\KatlaSpace {}\IdrisBound {xs}\KatlaSpace {}\IdrisFunction {++}\KatlaSpace {}\IdrisFunction {reverse}\KatlaSpace {}\IdrisBound {xs}\KatlaNewline {}
5454\end {SaveVerbatim }
@@ -87,7 +87,7 @@ \section{Inline Code}\label{inline-code}}
8787
8888By using the \texttt {expr } class, we can write a block expression:
8989
90- \let\KatlaSnippet\relax {}\newcommand \KatlaSnippet [1][]{\UseVerbatim [#1]{KatlaSnippet}}
90+ \let\KatlaSnippet\relax {}\newcommand \KatlaSnippet [1][]{\BUseVerbatim [#1]{KatlaSnippet}}
9191\begin {SaveVerbatim }[commandchars=\\ \{\} ]{KatlaSnippet}
9292\IdrisData {[}\KatlaNewline {}
9393\KatlaSpace {}\KatlaSpace {}\KatlaSpace {}\KatlaSpace {}\IdrisData {1,}\KatlaNewline {}
@@ -136,7 +136,7 @@ \section{Multiple Files}\label{multiple-files}}
136136\end {SaveVerbatim }
137137\KatlaSnippet {}.
138138
139- \let\KatlaSnippet\relax {}\newcommand \KatlaSnippet [1][]{\UseVerbatim [#1]{KatlaSnippet}}
139+ \let\KatlaSnippet\relax {}\newcommand \KatlaSnippet [1][]{\BUseVerbatim [#1]{KatlaSnippet}}
140140\begin {SaveVerbatim }[commandchars=\\ \{\} ]{KatlaSnippet}
141141\IdrisKeyword {failing}\KatlaSpace {}\IdrisData {"Undefined\KatlaSpace {}name\KatlaSpace {}Vect."}\KatlaNewline {}
142142\KatlaSpace {}\KatlaSpace {}\KatlaSpace {}\KatlaSpace {}\IdrisFunction {f}\KatlaSpace {}\IdrisKeyword {:}\KatlaSpace {}Vect\KatlaSpace {}n\KatlaSpace {}a\KatlaSpace {}\IdrisKeyword {\KatlaDash {}>}\KatlaSpace {}Vect\KatlaSpace {}\IdrisKeyword {(}n\KatlaSpace {}+\KatlaSpace {}n\IdrisKeyword {)}\KatlaSpace {}a\KatlaNewline {}
@@ -150,7 +150,7 @@ \section{Packages}\label{packages}}
150150using the \texttt {idris2-packages } key. For example, adding
151151\texttt {contrib } allows us to use the \texttt {Language.JSON } module.
152152
153- \let\KatlaSnippet\relax {}\newcommand \KatlaSnippet [1][]{\UseVerbatim [#1]{KatlaSnippet}}
153+ \let\KatlaSnippet\relax {}\newcommand \KatlaSnippet [1][]{\BUseVerbatim [#1]{KatlaSnippet}}
154154\begin {SaveVerbatim }[commandchars=\\ \{\} ]{KatlaSnippet}
155155\IdrisKeyword {import}\KatlaSpace {}\IdrisModule {Language.JSON}\KatlaNewline {}
156156\KatlaNewline {}
0 commit comments