calc but for compositions

Stream: new members

[Paul Nelson]

Is there something analogous to calc but for compositions, that would make the following (broken) code work?

import Mathlib

example
    (A B C : Type)
    (f : A → B)
    (g : B → C)
    : (A → C) := by
  calc
    A → B := f        -- invalid 'calc' step, relation expected A → B
    _ → C := g

example
    (R : Type) [CommRing R]
    (A : Type) [AddCommGroup A] [Module R A]
    (B : Type) [AddCommGroup B] [Module R B]
    (C : Type) [AddCommGroup C] [Module R C]
    (f : A →ₗ[R] B)
    (g : B →ₗ[R] C)
    : (A →ₗ[R] C) := by
  calc
    A →ₗ[R] B := f
    _ →ₗ[R] C := g

[Eric Rodriguez]

The first one should work already! The second one is a bit broken right now IIRC but is meant to be in scope for calc.

[Paul Nelson]

I edited it to add the error message for the first one as a comment

[Eric Wieser]

#6509 contains a recipe for how to make the second one work

[Paul Nelson]

ah, great

[Alex J. Best]

The first came up before, https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/calc.20mode.20for.20types/near/383739924, but I'm not sure if it was ever reported upstream @Eric Wieser

[Eric Wieser]

Nope, I never did file an issue for that