Commit 2020-01-30 00:09 868333b9

View on Github →

feat(data/W): show finitely branching W types are encodable (#1817)

  • feat(data/equiv,data/fintype): an encodable fintype is equiv to a fin
  • feat(data/W): finitely branching W types are encodable
  • feat(archive/examples/prop_encodable): show a type of propositional formulas is encodable
  • fix(data/W): remove unused type class argument
  • fix(data/equiv): add two docstrings
  • fix(*): multiple fixes from code review

Estimated changes

added def mk_fn0
added def mk_fn1
added def mk_fn2
added inductive prop_form
added def W.depth
added theorem W.depth_lt_depth_mk
added theorem W.depth_pos
added inductive W