W types #

The file Mathlib/Data/W/Basic.lean shows that if α is an encodable fintype and for every a : α, β a is encodable, then W β is encodable.

As an example of how this can be used, we show that the type of propositional formulas with variables labeled from an encodable type is encodable.

The strategy is to define a type of labels corresponding to the constructors. From the definition (using sum, unit, and an encodable type), Lean can infer that it is encodable. We then define a map from propositional formulas to the corresponding Wfin type, and show that map has a left inverse.

We mark the auxiliary constructions private, since their only purpose is to show encodability.

inductive PropEncodable.PropForm (α : Type u_1) :
Type u_1

Propositional formulas with labels from α.

Instances For

    The next three functions make it easier to construct functions from a small Fin.