Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-29 16:24 07cdafe9

View on Github →

feat(tactic/with_local_reducibility): alter reducibility attributes locally (#2820)

Estimated changes

Modified src/tactic/core.lean

Created src/tactic/with_local_reducibility.lean

added def tactic.decl_reducibility.to_attribute

added inductive tactic.decl_reducibility

Created test/with_local_reducibility.lean

added def test.wlr_irred

added def test.wlr_red

added def test.wlr_semired