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) }}
```

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

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

Interesting, thanks!

James Wood has marked this topic as resolved.

Last updated: Feb 05 2023 at 14:02 UTC