Stream: Elpi users & devs

Topic: ✔ Spilling under a binder


view this post on Zulip Enrico Tassi (May 11 2022 at 08:31):

No that I know of, it just felt natural to implement it in Elpi. Later Dale and Ulisses did something similar, but in the reasoning logic of Abella here. Since there are too many "not implemented" in my code, I never tried to publish it.

On the side, the feature is quite advanced wrt the coq embedding, for example if you spill under a coq binder you get the expected context, eg

R = {{ forall x : nat, lp:{{   {foo}  }}  }}

you should get something like

(pi x\ decl x `x` {{ nat }} => foo (TMP x)),
R = {{ forall x : nat, lp:(TMP x) }}

view this post on Zulip Enrico Tassi (May 11 2022 at 08:32):

But I rarely use that feature myself, while @Cyril Cohen does.

view this post on Zulip Enrico Tassi (May 11 2022 at 08:34):

Anyway, feedback on the feature is welcome. Even more understanding/implementing the missing cases ;-)

view this post on Zulip James Wood (May 11 2022 at 08:42):

Interesting, thanks!

view this post on Zulip Notification Bot (May 11 2022 at 08:42):

James Wood has marked this topic as resolved.


Last updated: Feb 05 2023 at 14:02 UTC