Default structure value in mutual block

Stream: new members

[Eric Paul]

I would like the default value of b in the structure B to be A.a but I get the error Invalid field notation: Type is not of the form ``C ...`` where C is a constant.

mutual
inductive A where
| a : A

structure B where
  b : A := A.a
end

The mutual block is not needed here, but in my actual use it is. Is there a way to set a default value here?

[Kyle Miller]

Sorry, inside a mutual block the only thing that's supported is referring to the types, not the constructors.

Could you say more about your use case for wanting this?

A semi-workaround is that you could do something like

mutual
inductive A where
| a : A

structure B' where
  b : A
end

structure B extends B' where
  b : A := A.a

and then, perhaps, make a coercion from B to B'.

[Robin Arnez]

You can also use tactics:

mutual
inductive A where
| a : A

structure B where
  b : A := by exact .a
end

That way it will only ever be elaborated when you construct a value of type B.

[Eric Paul]

Thanks to the both of you for the useful info! That tactic approach is sneaky!