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

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_pos
added inductive W_type