I'm very puzzled by the usage of `Constr.Unsafe.occurn`

(context: I am trying to use it to detect whether a `Prod b t`

is dependent or not, by detecting whether `Rel 0`

appears in `t`

). But I really don't understand what the behaviour of that function is.

```
From Ltac2 Require Import Ltac2.
Ltac2 Eval Constr.Unsafe.occurn 0 '(nat). (* nat is closed, yet this returns true *)
Ltac2 Eval Constr.Unsafe.occurn 0 (Constr.Unsafe.make (Constr.Unsafe.Rel 1)). (* this is true despite (Rel 1) clearly not containing (Rel 0) *)
Ltac2 Eval Constr.Unsafe.occurn 0 (Constr.Unsafe.make (Constr.Unsafe.Rel 0)). (* this is false, I am starting to think the boolean is just flipped? *)
Ltac2 Eval Constr.Unsafe.occurn 0 '(forall A B, B). (* this is true, as expected with a flipped boolean *)
Ltac2 Eval Constr.Unsafe.occurn 0 '(forall A B, A). (* this is false? Would this mean there is no lifting happening when going under a binder? *)
```

My experiments lead me to conclude that the documentation mentions the test the wrong way around, and does not use any lifting when going under a binder, is that indeed the case? Back to my first question, how can I detect whether a `Prod`

is dependent or not?

it is flipped, but note that rels are 1-based so `occurn 0`

returns nonsense

Ha !

I was too bold in assuming it was the same as in MetaCoq

Thanks

Meven Lennon-Bertrand has marked this topic as resolved.

Last updated: Oct 12 2024 at 12:01 UTC