English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

The set of integer number lists with finite length, and the set of binarytrees with integer labels are both countably infinite. Many inductively definedtypes also have countably many elements. In this paper, we formalize the syntaxof first order inductive definitions in Coq and prove them countable, undersome side conditions. Instead of writing a proof generator in a meta language,we develop an axiom-free proof in the Coq object logic. In other words, ourproof is a dependently typed Coq function from the syntax of the inductivedefinition to the countability of the type. Based on this proof, we provide aCoq tactic to automatically prove the countability of concrete inductive types.We also developed Coq libraries for countability and for the syntax ofinductive definitions, which have value on their own.

Countability of Inductive Types Formalized in the Object-Logic Level