• coherent_domain
    link
    fedilink
    English
    arrow-up
    2
    ·
    7 days ago

    Coinduction works on some uncountable set, for example, streams (or infinite list) which are A^{nat}, where A is the type of the elements in the stream. It looks a bit like induction on finite list, but slightly different.