Mathlib v3 is deprecated. Go to Mathlib v4

Inductive tactic.decl_reducibility

Modification history

2020-05-29 16:24

src/tactic/with_local_reducibility.lean

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

Added tactic.decl_reducibility View on Github →