Getting the instance name from a call

Stream: lean4

[Leni Aniva]

Is there a function which takes an expression of the form

@HAppend.hAppend (List Nat) (List Nat) (List Nat) (@instHAppendOfAppend (List Nat) (@List.instAppend Nat))

and returns List.instAppend Nat, and vice versa?

Similarly it should convert between

@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat)
instAddNat

The idea is to convert between an instance and a function call to a class function

[Leni Aniva]

If this is impossible is there a way to extract the implicit components? e.g.

@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) x y z

turns into

@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat)

The use case is I need to convert a instance function invocation into a unique symbol for usage in SMT solvers, for example the above would be mapped to nat.+

[Marcus Rossel]

Leni Aniva said:

Is there a function which takes an expression of the form

@HAppend.hAppend (List Nat) (List Nat) (List Nat) (@instHAppendOfAppend (List Nat) (@List.instAppend Nat))

and returns List.instAppend Nat, and vice versa?

Do you really want List.instAppend, or rather List.append?

[Leni Aniva]

Marcus Rossel said:

Leni Aniva said:

Is there a function which takes an expression of the form

@HAppend.hAppend (List Nat) (List Nat) (List Nat) (@instHAppendOfAppend (List Nat) (@List.instAppend Nat))

and returns List.instAppend Nat, and vice versa?

Do you really want List.instAppend, or rather List.append?

both will work, I just need something to pinpoint each HAppend.hAppend (or HAdd.hAdd) function call down to one or two unique symbols

come to think of it even @HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) will be fine