# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1423818607 -32400
# Node ID 4f1107f1f6aaed73d3d79704077edab557cbad31
# Parent  b7e693b6d7d976bfff0fb11463d5bf4c24c4f082
Fix source

diff -r b7e693b6d7d9 -r 4f1107f1f6aa agda.tex
--- a/agda.tex	Fri Feb 13 17:51:57 2015 +0900
+++ b/agda.tex	Fri Feb 13 18:10:07 2015 +0900
@@ -421,7 +421,7 @@
 等式の証明には agda の standard library における Relation.Binary.Core の定義を用いる。
 
 \begin{table}[html]
-    \lstinputlisting[label=src:equiv, caption= Relation.Binary.Core による等式を示す型 $ \equiv $] {src/equiv.agda}
+    \lstinputlisting[label=src:equiv, caption= Relation.Binary.Core による等式を示す型 $ \equiv $] {src/equiv.agda.replaced}
 \end{table}
 等式は等式を示すデータ型 $ \equiv $ により定義される。
 $ \equiv $ は同じ両辺が同じ項に簡約される時にコンストラクタ refl で構築できる。