Mercurial > hg > Papers > 2015 > atton-thesis
comparison agda.tex @ 36:2ff5acb0d2e9
Add escape script
| author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 12 Feb 2015 17:44:18 +0900 |
| parents | c684abcc781b |
| children | 470d99799398 |
comparison
equal
deleted
inserted
replaced
| 35:7efeca634b50 | 36:2ff5acb0d2e9 |
|---|---|
| 503 最終的に等式の左辺を $ \blacksquare $ の項へと変形することで等式の証明が得られる。 | 503 最終的に等式の左辺を $ \blacksquare $ の項へと変形することで等式の証明が得られる。 |
| 504 | 504 |
| 505 自然数の加法の交換法則を $ \equiv $-Reasoning を用いて証明した例がリスト\ref{src:nat_add_sym_reasoning}である。 | 505 自然数の加法の交換法則を $ \equiv $-Reasoning を用いて証明した例がリスト\ref{src:nat_add_sym_reasoning}である。 |
| 506 特に n と m が1以上である時の証明に注目する。 | 506 特に n と m が1以上である時の証明に注目する。 |
| 507 | 507 |
| 508 % TODO: FIXME: unicode char | 508 \begin{table}[html] |
| 509 \begin{table}[html] | 509 \lstinputlisting[label=src:nat_add_sym_reasoning, caption= $ \equiv $ - Reasoning を用いた証明の例] {src/nat_add_sym_reasoning.agda.replaced} |
| 510 \lstinputlisting[label=src:nat_add_sym_reasoning, caption= $ \equiv $ - Reasoning を用いた証明の例] {src/nat_add_sym_reasoning.agda} | |
| 511 \end{table} | 510 \end{table} |
| 512 | 511 |
| 513 まず \verb/ (S n) + (S m)/ は + の定義により \verb/ S (n + (S m)) / に等しい。 | 512 まず \verb/ (S n) + (S m)/ は + の定義により \verb/ S (n + (S m)) / に等しい。 |
| 514 よって refl で導かれる。 | 513 よって refl で導かれる。 |
| 515 なお、基本的に定義などで同じ項に簡約される時は refl によって記述することが多い。 | 514 なお、基本的に定義などで同じ項に簡約される時は refl によって記述することが多い。 |