Stream: Elpi users & devs

Topic: Typeclass instanciation via elpi

Quentin VERMANDE (Oct 23 2023 at 09:28):

Hi. I have seen in coq-elpi/apps that the predicate coercion is called whenever Coq fails to solve a coercion problem. Is it possible to do the same thing when Coq fails to solve a typeclass instanciation problem?

Pierre Roux (Oct 23 2023 at 10:38):

The specialist here is @Davide F

Cyril Cohen (Oct 23 2023 at 10:55):

@Quentin VERMANDE I think we should ask @Davide F about LPCIC/coq-elpi#522

Quentin VERMANDE (Oct 23 2023 at 11:06):

Actually, we already talked about it, and he has not worked on what I need. His work calls a tactic explicitly, whereas I need my (future) code to be called automatically when Coq receives a term to elaborate.

Cyril Cohen (Oct 23 2023 at 11:10):

I do not understand how it does not cover what you need. Isn't Elpi Override TC TC_solver All. what you need?

Cyril Cohen (Oct 23 2023 at 11:13):

cf this code

Cyril Cohen (Oct 23 2023 at 11:15):

and this example of use

Cyril Cohen (Oct 23 2023 at 11:16):

Cyril Cohen said:

and this example of use

where solve is the elpi tactic called implicitly instead of standard class resolution.

Notification Bot (Oct 24 2023 at 13:54):

Quentin VERMANDE has marked this topic as unresolved.

Last updated: Oct 13 2024 at 01:02 UTC