Mathlib v3 is deprecated. Go to Mathlib v4

Def tactic.decl_reducibility.to_attribute

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.to_attribute View on Github →