Mercurial > hg > Papers > 2015 > atton-thesis
changeset 44:4f1107f1f6aa
Fix source
| author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 13 Feb 2015 18:10:07 +0900 |
| parents | b7e693b6d7d9 |
| children | 12c5e455fe55 |
| files | agda.tex |
| diffstat | 1 files changed, 1 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- 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 で構築できる。