W types #
Given α : Type
and β : α → Type
, the W type determined by this data, WType β
, 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 WType β
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 WType
is somewhat verbose, it is preferable to putting a single character
identifier W
in the root namespace.
Given β : α → Type*
, WType β
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
.
Instances For
The canonical map from WType β
into any type γ
given a map (Σ a : α, β a → γ) → γ
.
Equations
- WType.elim γ fγ (WType.mk a f) = fγ { fst := a, snd := fun b => WType.elim γ fγ (f b) }
Instances For
The depth of a finitely branching tree.
Equations
- WType.depth (WType.mk a f) = (Finset.sup Finset.univ fun n => WType.depth (f n)) + 1