tactic.elide - mathlib3 docs

meta def tactic.elide.unelide (e : expr) :

meta def tactic.interactive.elide (n : interactive.parse lean.parser.small_nat) (loc : interactive.parse interactive.types.location) :

tactic unit

The elide n (at ...) tactic hides all subterms of the target goal or hypotheses beyond depth n by replacing them with hidden, which is a variant on the identity function. (Tactics should still mostly be able to see through the abbreviation, but if you want to unhide the term you can use unelide.)

source

meta def tactic.interactive.unelide (loc : interactive.parse interactive.types.location) :

tactic unit

The unelide (at ...) tactic removes all hidden subterms in the target types (usually added by elide).

source

def tactic_doc.tactic.elide / unelide :

tactic_doc_entry

The elide n (at ...) tactic hides all subterms of the target goal or hypotheses beyond depth n by replacing them with hidden, which is a variant on the identity function. (Tactics should still mostly be able to see through the abbreviation, but if you want to unhide the term you can use unelide.)

The unelide (at ...) tactic removes all hidden subterms in the target types (usually added by elide).