Commit 2020-11-04 21:59 189063b1

View on Github →

chore(data/W): rename W to W_type (#4909) Having a single character identifier in the root namespace is inconvenient. closes leanprover-community/doc-gen#83

Estimated changes

Modified archive/examples/prop_encodable.lean

Modified docs/overview.yaml

Modified src/data/W.lean

deleted def W.depth

deleted theorem W.depth_lt_depth_mk

deleted theorem W.depth_pos

deleted inductive W

added def W_type.depth

added theorem W_type.depth_lt_depth_mk

added theorem W_type.depth_pos

added inductive W_type

Modified src/data/pfunctor/univariate/basic.lean

modified def pfunctor.W