t0_ToC.v

(* Coco tutorial 0: Table of Contents *)

(** Coco is a Rocq library designed for defining corecursive functions.
  This tutorial serves as a comprehensive guide for users who want to understand and utilize Coco. *)

(** The tutorial is located in [/src/tutorial] and consists of the following files:

  [t0_ToC.v] : Table of Contents

  [t1_SynGuard.v] : Syntactic Guard and Productivity

  [t2_FO.v] : First Order Productivity

  [t3_SO.v] : Second Order Productivity

  [t4_SPE.v] : Coinductive Types and Semantic Polynomial Endofunctor

  [t5_Bisim.v] : Bisimulation and Coinductive Proofs

  [t6_Indexed.v] : Indexed Coinductive Types and their Corecursive Functions

  [t7_Extend1.v] : Extending Coco with New Function Combinators

  [t8_Extend2.v] : Extending Coco with New CTTs and STTs

  [t9_SAcc.v] : Productivity with Semi Well Founded Order *)

(** Recommended Reading Paths:

  1. For users wanting to define new corecursive functions with existing Coco-defined coinductive types:
    - Read tutorials [t1_SynGuard.v] through [t3_SO.v]

  2. For users wanting to define new coinductive types using Coco:
    - Read tutorials [t1_SynGuard.v] through [t5_Bisim.v]

  3. For working with indexed (dependent) coinductive types:
    - Read [t6_Indexed.v]

  4. For users interested in extending the Coco library:
    - Read tutorials [t7_Extend1.v] and [t8_Extend2.v]

  5. Advanced Topic:
    - [t9_SAcc.v] covers semi-well-founded order as a generalization of 1-productivity
    - Most corecursive functions which are not recursive-corecursive can be defined without this knowledge *)

(** There are some exercises in the tutorials. You can find solutions at files in [/src/example]. *)