Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-08-20 12:14 87714320

View on Github →

doc(tactic/ring2): document parts of ring2 (#1208)

  • doc(tactic/ring2): document parts of ring2
  • feat(data/tree): refactor binary trees into their own module
  • feat(tactic/ring2): resolve correct correctness
  • chore(tactic/ring2): move copyright into comment
  • doc(tactic/ring2): wording

Estimated changes

added def tree.get
added def tree.get_or_else
added def tree.index_of
added def tree.map
added def tree.of_rbnode
added def tree.repr
added inductive {u}
deleted def linarith.tree.repr
deleted inductive linarith.{u}
deleted inductive tactic.ring2.{u}