35 |
35 |
36 <p> |
36 <p> |
37 The key notion underlying the package is that of a <i>bounded natural functor</i> |
37 The key notion underlying the package is that of a <i>bounded natural functor</i> |
38 (<i>BNF</i>)—an enriched type constructor satisfying specific properties |
38 (<i>BNF</i>)—an enriched type constructor satisfying specific properties |
39 preserved by interesting categorical operations (composition, least fixed point, |
39 preserved by interesting categorical operations (composition, least fixed point, |
40 and greatest fixed point). The <tt>Basic_BNFs.thy</tt> and <tt>More_BNFs.thy</tt> |
40 and greatest fixed point). The <tt>Basic_BNFs.thy</tt>, <tt>More_BNFs.thy</tt>, |
41 files register various basic types, notably for sums, products, function spaces, |
41 and <tt>Countable_Set_Type.thy</tt> files register various basic types, notably |
42 finite sets, multisets, and countable sets. Custom BNFs can be registered as well. |
42 for sums, products, function spaces, finite sets, multisets, and countable sets. |
|
43 Custom BNFs can be registered as well. |
43 |
44 |
44 <p> |
45 <p> |
45 <b>Warning:</b> The package is under development. Please contact any nonempty |
46 <b>Warning:</b> The package is under development. Please contact any nonempty |
46 subset of |
47 subset of |
47 <a href="mailto:traytel@in.tum.de">the</a> |
48 <a href="mailto:traytel@in.tum.de">the</a> |