W types #
Given α : Type
and β : α → Type
, the W type determined by this data, W_type β
, 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_type β
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.
Implementation details #
While the name W_type
is somewhat verbose, it is preferable to putting a single character
identifier W
in the root namespace.
Given β : α → Type*
, W_type β
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
.
Equations
W_type
is encodable when α
is an encodable fintype and for every a : α
, β a
is
encodable.