trans does not work on implicit arguments #1222
Description
import Batteries.Tactic.Trans
inductive A (α : Type) where
| mk : α → A α
inductive r {α} : A α → A α → Prop where
| trans {a b c} : r a b → r b c → r a c
attribute [trans] r.trans
set_option trace.Tactic.trans true
example {α} {a b c : A α} : r a c := by
trans bgives
α : Type
a b c : A α
⊢ r a c
[Tactic.trans] goal decomposed
[Tactic.trans] rel:
@r
[Tactic.trans] x:
a
[Tactic.trans] z:
c
[Tactic.trans] trying homogeneous case
[Tactic.trans] trying lemma Trans.simple
It looks like rel here should be @r α instead of @r. If the index is explicit, trans succeed:
inductive r' (α) : A α → A α → Prop where
| trans {a b c} : r' α a b → r' α b c → r' α a c
attribute [trans] r'.trans
example {α} {a b c : A α} : r' α a c := by
trans b -- succeed