Quentin VERMANDE (Oct 25 2023 at 06:45): Quentin VERMANDE (Oct 25 2023 at 06:45):Hi. Using Coercion, it is possible to declare a coercion from a class C to the special class Funclass, so that any term of type C can be used as a function. Is there an equivalent in elpi (using if possible the predicate coercion from coq-elpi)?
Pierre Roux (Oct 25 2023 at 06:50):https://github.com/LPCIC/coq-elpi/blob/master/coq-builtin.elpi#L1152-L1169
Quentin VERMANDE (Oct 25 2023 at 06:52):Oh thanks.
Notification Bot (Oct 25 2023 at 06:52):Quentin VERMANDE has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC