Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-10-01 18:48 5ed5f594

View on Github →

feat(tactic/delta_instance): handle parameters and use in library (#1483)

  • feat(tactic/core): improve delta_instance handler
  • feat(*): use delta_instance derive handler
  • feat(tactic/delta_instance): cleaner handling of application under binders
  • Revert "feat(tactic/delta_instance): cleaner handling of application under binders" This reverts commit 4005a2fad571bf922c98f94cbc1154666abc259d.
  • comment apply_under_pis
  • properly get unused name
  • feat(tactic/delta_instance): run with high priority and don't run on inductives
  • Update src/tactic/core.lean Co-Authored-By: Floris van Doorn

Estimated changes

added inductive P
added def S
added def X
added def id_ring