Hello!

I don't understand the use of the external function `occurs`

, as I tried it on a simple example.

The documentation says that the first argument should be a constant (so I guess either a global reference or a variable) and the error message says that the second argument should be a constant.

My code is:

```
Definition foo := nat -> nat.
Elpi Query lp:{{
occurs {{nat}} {{foo}}.
}}.
```

and the message is : `The second argument of occurs must be a constant`

, but `foo`

is a constant and I don't understand why the documentation mentions the first and not the second argument.

Thanks in advance for your help

Sorry the doc is written in the context of `elpi`

alone, without Coq. An elpi contant is a symbol like `foo`

while `{{ nat }}`

, which is a Coq constant in some sense, unravels to `global (indt "Coq.Init.Datatypes...")`

which is not a constant in the first sense.

a not very efficient way to test what you want is

```
(pi x\ copy {{ nat }} x => copy T T1)
```

since `T1`

does not see `x`

the goal fails if `T`

did contain `{{nat}}`

, since it was replaced by `x`

, and hence the copied term cannot be assigned to `T1`

.

That can be made more efficient by writing a predicate similar to copy which does not really copy the term, but just fail if a predicate holds on any subterm, eg

```
pred anywhere i:(term -> prop), i:term.
anywhere P T :- P T, !, fail.
anywhere P (app L) :- forall L (anywhere P).
...
```

and pass `t\ t = {{ nat }}`

as `P`

.

Thank you, so I have another question. `occurs`

is used there : https://github.com/LPCIC/coq-elpi/blob/fe9cdf7ae78f56980266cde47bae5f757c1a1739/apps/derive/elpi/projK.elpi#L47 and I don't understand exactly how this works because it seems to deal with Coq constants and not elpi ones.

And if I understood you well, `occurs`

cannot be used to check if a specific reified Coq term occurs in another?

This is just "an illusion" because the types are not helping. There is an invariant that the term is an elpi constant, a name in particular. See

how I fill the list in here: https://github.com/LPCIC/coq-elpi/blob/fe9cdf7ae78f56980266cde47bae5f757c1a1739/apps/derive/elpi/projK.elpi#L79

`x`

is an elpi constant (of type term), which one can use with `occur`

.

Maybe my terminology in the doc of elpi is not clear, `occurs`

works for "names", like the "x" in `pi x\`

, sometimes these things are called eigenvariables, or nominal constants.

The valid argument of `occur`

is not determined by its type, but rather by its value. If the value is a constant (an atom), then it is ok. If it is a compound syntax tree, then it is not. The type of the value can by arbitrary.

Sorry for the confusion, I'd be happy to apply any suggestion to the doc of `occurs`

.

Okay I understand better now! I think that the error message was confusing for me because it mentions the second argument of `occurs`

while the doc mentions the first one, so my suggestion would be to clarify a bit this point if you can

Otherwise your documentation was clear and I just missed the meaning of eigenvariable, thank you very much !

Last updated: Jun 14 2024 at 19:02 UTC