Should I be using classes here?

Stream: new members

[Vaibhav Karve]

I have the following MWE:

structure A :=
(f : nat -> nat)

structure B extends A :=
(g : nat -> nat)

Now I want to define a new function h : A -> nat which behaves differently if the argument is actually of type B. Ho do I do it?

[Reid Barton]

The argument to h can't be of type B, it is of type A.

[Reid Barton]

You could say "behaves differently when called in the form h (B.to_A b)", but then it is clearly absurd.

[Reid Barton]

Probably you want an inductive type with multiple constructors.

[Vaibhav Karve]

Instead of making inductive types can I somehow have just h be an inductive definition?

[Vaibhav Karve]

Asked another way, can I check for "does my type have g as a field, if yes then do X else do Y"?

[Reid Barton]

Again the type never has g as a field because the type is A.
You could make h a member of class, and both A and B instances, I suppose. Then the data of what h should do is supplied by instance inference.

[Reid Barton]

A value a : A is completely determined by a.f, so you can never tell if it was "originally" obtained from some b : B

[Vaibhav Karve]

Reid Barton said:

A value a : A is completely determined by a.f, so you can never tell if it was "originally" obtained from some b : B

Thanks, that makes it clearer. Does that change if I had defined A and B as classes intead of structures?

[Reid Barton]

Nope

[Vaibhav Karve]

Thanks.