Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-05-08 11:42 c9cfafc9

View on Github →

chore(tactics): splitting tactics and tests into more files (#985)

  • chore(tactics): splitting tactics and tests into more files, cleaning up dependencies
  • tweaking comment
  • introducing tactic.basic and fixing imports
  • fixes
  • fix copyright
  • fix some things

Estimated changes

added structure dependent_fields
added theorem df.ext
added def my_bar
added def my_foo
added theorem unit.ext
deleted structure dependent_fields
deleted theorem df.ext
deleted def my_bar
deleted def my_foo
deleted theorem unit.ext