unused variable on structure instances

Stream: lean4

[Matthew Ballard]

structure A where

structure B extends A where

def a : A := sorry

def b : B := {a, a with}

doesn't trigger the unused variable linter.

Is this intentional?

[Alex J. Best]

Syntactically this is very different to an unused variable, so I imagine it is intentional inasmuch as this just isnt what that linter was designed to do.

[Matthew Ballard]

Fair point. The question arose because of what the syntax gets transformed into. Here is a modification of the example to not be so degenerate:

structure A where
  x : Nat

structure B extends A where

def a : A := ⟨0⟩

def a' : A := ⟨1⟩

def b : B := {a, a' with}

#print b
-- def b : B :=
-- let src := a;
-- let src_1 := a';
-- { toA := { x := src.x } }

[Alex J. Best]

I agree that it is a weird term. In the lean 3 days I wrote an "unused term mode let" linter. But iirc it had too many (false?) positives, due to TC putting lots of lets in the terms that weren't used later.