Add Agda pygments highlighter

chapters/martin-lof.tex

@@ -357,22 +357,22 @@ \subsection{Agda}
 用户可以让Agda执行一些操作修改洞附近的代码, 在这个与
 软件合作的过程中逐步完成整个证明. 譬如证明定理
 \(\forall n. n + 0 = n\).
-\begin{verbatim}
+\begin{minted}{agda}
 theorem : (n : Nat) -> n + 0 == n
 theorem = ?
-\end{verbatim}
+\end{minted}
 这里的问号就是待填入的内容. 此时可以使用快捷键
 命令Agda引入变量, 它便会自动将代码修改为
-\begin{verbatim}
+\begin{minted}{agda}
 theorem : (n : Nat) -> n + 0 == n
 theorem n = ?
-\end{verbatim}
+\end{minted}
 接下来, 我们命令Agda对\(n\)归纳, 代码就会变为
-\begin{verbatim}
+\begin{minted}{agda}
 theorem : (n : Nat) -> n + 0 == n
 theorem zero = ?
 theorem (succ x) = ?
-\end{verbatim}
+\end{minted}
 以此类推. 由于这里类型系统强大的表达能力, 我们可以
 直接使用类型指导应该填入哪些东西.