I guess this is a silly beginner question, but I don't quite understand how I would write a function which inspects the term under a binder. The Elpi term constructor for a product term is:

```
type prod name -> term -> (term -> term) -> term. % forall x : t,
```

I don't understand how I can use the 3rd argument of type `term -> term`

in e.g. a recursive call of a fold term function without something like a quod libet sandbox. Say I have a Coq term `forall (x:False), some_term`

how can I look into `some_term`

without providing a term of type `False`

as argument to the `term -> term`

thing?

In Ltac2 this is quite obvious. The `kind`

constructor for a product is `Prod (binder, constr)`

where `binder`

is an opaque type with some functions to access the variable name and type. For the body I get a `constr`

and I can look at it without providing an argument.

What I want to do is collect all arguments of a specific constructor in a term as list.

There are some hints in this tutorial: https://lpcic.github.io/coq-elpi/tutorial_elpi_lang.html#higher-order-features, in particular the language gives you `pi x\`

and `=>`

. The idea is that `pi`

postulates a fresh name `x`

, and you can pass that to the term of type `term -> term`

in order to get the body where the bound variable was replaced a by a fresh name `x`

.

```
under (app _ as T) :- coq.say T.
under (prod _ _ F) :- pi x\ under (F x).
```

Since `x`

is fresh, no program clause (static clause) can mention it, so you can attach some knowledge to `x`

via `=>`

. Typically you would attach to `x`

its type.

```
under (app _ as T) :- coq.say T.
under (prod N S F) :- pi x\ decl x N S => under (F x).
```

This is so common that there is a macro

```
under (app _ as T) :- coq.say T.
under (prod N S F) :- @pi-decl N S x\ under (F x).
```

It is important to attach `decl`

to `x`

, since it is part of the encoding of coq terms. If you call deep under the binder the coq type checker or even the pretty printer, it would use these clauses to know how to type/print `x`

.

This is a really good beginner question, I hope it is somehow covered by the first tutorial. Are you following them in linear order of you started from the Coq ones? If so, I may need to add backporinters, since this way of traversing terms is really of paramount importance.

Thanks for the details! I followed the tutorials in linear order, but i must admit I saved the section "higher-order-features" for later and then didn't come back to it after I went through the other tutorials. So I missed the "quod libet sandbox operator" `pi`

.

Here and there some application examples would help. E.g. the HOAS tutorial doesn't define a single predicate (afair). Also I don't think I found non trivial examples for matching on Coq terms.

But all in all the tutorial is very good, understandable and to the point.

I will ask a related question. Do all the local variables introduced with `pi`

have to be given a type if the typechecker is called somewhere below?

I am usually giving a type to things that are likely to be involved in typechecking later, but I also have to quantify over some temporary variables that I eventually remove by substitution with `copy`

. Surprisingly, when typechecking a term that has nothing to do with these temporary variables, I get a message like `Bound variable c8 not found in the Coq context`

, suggesting that the whole Elpi context is given to Coq, and thus must be typed, even the terms that won't be used by the typechecker. Am I right? I guess it's because Elpi cannot know what will be done on the Coq side, so it gives the full context, right?

Btw.: In Ltac2 the bound term is pretty printed as follows:

```
Require Import Ltac2.Ltac2.
Require Import Ltac2.Printf.
Ltac2 Eval match (Constr.Unsafe.kind '(fun x => S x)) with
| Constr.Unsafe.Lambda b c => printf "%t" c
| _ => printf "other"
end.
```

gives

```
(S _UNBOUND_REL_1)
- : unit = ()
```

I guess it's because Elpi cannot know what will be done on the Coq side, so it gives the full context, right?

Exactly. Also if you have a hole, then it is likely to see the whole context, including the variables which you did not type.

it is a trade off, either the context is manually managed... or it is implicit, but in that case Elpi can't second guess you

It's ok there is still the workaround `@pi-decl N (sort prop) x\`

if I know variable `x`

will not appear in typechecked terms, and has a type that is complex and that I don't want to generate

(should probably create a predicate called `dummy-type`

or something that makes it explicit it does not matter what is put here as long as it has a valid type for Coq)

yes

`@pi-dummy x\`

Last updated: Jun 06 2023 at 23:01 UTC