Mercurial > hg > Papers > 2023 > soto-master
changeset 20:bc0d518ed166
Fix
| author | soto <soto@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 03 Feb 2023 03:10:18 +0900 |
| parents | 76055a4c1dd2 |
| children | 19f19ec356f5 |
| files | Paper/master_paper.pdf Paper/tex/agda.tex |
| diffstat | 2 files changed, 2 insertions(+), 2 deletions(-) [+] |
line wrap: on
line diff
--- a/Paper/tex/agda.tex Fri Feb 03 03:06:18 2023 +0900 +++ b/Paper/tex/agda.tex Fri Feb 03 03:10:18 2023 +0900 @@ -129,7 +129,7 @@ \subsection{自然数に0を足しても値が等しいことを証明するAgda} \coderef{proof}は型定義にも書いてあるとおり、自然数に0を足しても値が等しいことを証明するコードとなっている。 このように、Agda では証明したい論理式を型定義に書き、実装部分に当たる2行目以降に証明を書くことができる。 -\lstinputlisting[caption=等式変形の例,label=code:proof]{src/zero.agda.replaced} +\lstinputlisting[caption=自然数に0を足しても値が等しいことを証明するAgda,label=code:proof]{src/zero.agda.replaced} 実際にコードの中で行われている証明について説明する。 \{zero\}のパターンは$y$が0であったときの場合のことである。 @@ -163,7 +163,7 @@ 次に x が zero 以外の場合を考える。今回は ≡\verb/-Reasoning/ により式を展開している。 -\lstinputlisting[caption=congを用いた等式変形の例,label=code:agda-term-post]{src/agda-term3.agda.replaced} +\lstinputlisting[caption=加算の交換法則を証明するAgda,label=code:agda-term-post]{src/agda-term3.agda.replaced} これにより $ x + y \equiv y + x $ つまり $ (suc \: x) + y \equiv y + (suc \: x) $ を求めている 構文を説明すると、begin が始まりで $\blacksquare$ で終わりとなる。$\blacksquare$ は emacs-agda では $\backslash $qed で入力することができ、