Overload a function with a strucure and its extensions

Stream: new members

[Tianchen Zhao]

If I define a structure A and a map f on it, how can I overload f with B which extends A? Is there any good solutions to make f work for both A and B?

structure A := (pts : ℕ)
structure B extends A

variables (a : A) (b : B) (f : A → ℕ)

#check f a --ℕ
#check f b --type error

[Kevin Buzzard]

You can use a coercion to map A to B and define f from B to nat.

[Kevin Buzzard]

structure A := (pts : ℕ)
structure B extends A

instance : has_coe A B := ⟨λ a, { pts := a.pts }⟩

variables (a : A) (b : B) (f : B → ℕ)

#check f a -- ℕ
#check f b -- ℕ

[Kevin Buzzard]

or

structure A := (pts : ℕ)
structure B extends A

instance : has_coe B A := ⟨B.to_A⟩

variables (a : A) (b : B) (f : A → ℕ)

#check f a -- ℕ
#check f b -- ℕ