W types
Given α : Type and β : α → Type, the W type determined by this data, W β, is the inductively
defined type of trees where the nodes are labeled by elements of α and the children of a node
labeled a are indexed by elements of β a.
This file is currently a stub, awaiting a full development of the theory. Currently, the main
result is that if α is an encodable fintype and β a is encodable for every a : α, then W β
is encodable. This can be used to show the encodability of other inductive types, such as those
that are commonly used to formalize syntax, e.g. terms and expressions in a given language. The
strategy is illustrated in the example found in the file prop_encodable in the archive/examples
folder of mathlib.
Given β : α → Type*, W β is the type of finitely branching trees where nodes are labeled by
elements of α and the children of a node labeled a are indexed by elements of β a.
W is encodable when α is an encodable fintype and for every a : α, β a is
encodable.