inherit_doc doesn't know about alias

Stream: batteries

[Yaël Dillies]

I know that inherit_doc is defined in core and alias in batteries, but is there any chance we can get the following very reasonable example to work?

import Batteries.Tactic.Alias

/-- I have a docstring -/
def foo : True := trivial

@[inherit_doc] alias bar := foo
-- invalid `[inherit_doc]` attribute, could not infer doc source

[Mario Carneiro]

Probably (the implementation would be in batteries). The way other commands do this is to check for uses of the inherit_doc attribute and replace them by @[inherit_doc foo] as appropriate

[Floris van Doorn]

Mario Carneiro said:

The way other commands do this is to check for uses of the inherit_doc attribute and replace them by @[inherit_doc foo] as appropriate

This happens regularly? I do something like this in to_additive, and I thought it was a huge hack.

[Mario Carneiro]

eh, it felt like a hack to me too but it works

[Mario Carneiro]

I'm not really going to defend it since I'm the one who made it work like that

[Yaël Dillies]

Should I open an issue?