Meven Lennon-Bertrand (Mar 12 2024 at 17:46): Meven Lennon-Bertrand (Mar 12 2024 at 17:46):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?
Gaëtan Gilbert (Mar 12 2024 at 17:52):it is flipped, but note that rels are 1-based so occurn 0 returns nonsense
Meven Lennon-Bertrand (Mar 12 2024 at 17:56):Ha !
Meven Lennon-Bertrand (Mar 12 2024 at 17:56):I was too bold in assuming it was the same as in MetaCoq
Meven Lennon-Bertrand (Mar 12 2024 at 17:57):Thanks
Notification Bot (Mar 12 2024 at 17:57):Meven Lennon-Bertrand has marked this topic as resolved.
Last updated: Oct 12 2024 at 12:01 UTC