doc-src/ind-defs.toc
 author wenzelm Wed Oct 03 20:58:27 2001 +0200 (2001-10-03) changeset 11657 03c4a5c08a79 parent 294 058343877e3a permissions -rw-r--r--
*** empty log message ***
```     1 \contentsline {section}{\numberline {1}Introduction}{1}
```
```     2 \contentsline {section}{\numberline {2}Fixedpoint operators}{1}
```
```     3 \contentsline {section}{\numberline {3}Elements of an inductive or coinductive definition}{2}
```
```     4 \contentsline {subsection}{\numberline {3.1}The form of the introduction rules}{2}
```
```     5 \contentsline {subsection}{\numberline {3.2}The fixedpoint definitions}{3}
```
```     6 \contentsline {subsection}{\numberline {3.3}Mutual recursion}{3}
```
```     7 \contentsline {subsection}{\numberline {3.4}Proving the introduction rules}{4}
```
```     8 \contentsline {subsection}{\numberline {3.5}The elimination rule}{4}
```
```     9 \contentsline {section}{\numberline {4}Induction and coinduction rules}{4}
```
```    10 \contentsline {subsection}{\numberline {4.1}The basic induction rule}{4}
```
```    11 \contentsline {subsection}{\numberline {4.2}Mutual induction}{5}
```
```    12 \contentsline {subsection}{\numberline {4.3}Coinduction}{5}
```
```    13 \contentsline {section}{\numberline {5}Examples of inductive and coinductive definitions}{6}
```
```    14 \contentsline {subsection}{\numberline {5.1}The finite set operator}{6}
```
```    15 \contentsline {subsection}{\numberline {5.2}Lists of \$n\$ elements}{6}
```
```    16 \contentsline {subsection}{\numberline {5.3}A coinductive definition: bisimulations on lazy lists}{7}
```
```    17 \contentsline {subsection}{\numberline {5.4}The accessible part of a relation}{8}
```
```    18 \contentsline {subsection}{\numberline {5.5}The primitive recursive functions}{9}
```
```    19 \contentsline {section}{\numberline {6}Datatypes and codatatypes}{11}
```
```    20 \contentsline {subsection}{\numberline {6.1}Constructors and their domain}{11}
```
```    21 \contentsline {subsection}{\numberline {6.2}The case analysis operator}{11}
```
```    22 \contentsline {section}{\numberline {7}Conclusions and future work}{12}
```