Def takeImplicit

Modification history

2026-01-29 13:31

MathlibTest/apply_with.lean

feat(Tactic/ApplyWith): use a `config_elab` for `apply (config := cfg)` (#34524) …

Added takeImplicit View on Github →