Valerii Huhnin (Feb 20 2024 at 07:35): Valerii Huhnin (Feb 20 2024 at 07:35):In Ltac, when performing matching on terms, it is possible to access the context of the expression that was matched and then manipulate it using context tactic. Is it possible to check if the context is empty, i.e. that match happened at the top level of the term, i.e. that context ctxt [X] is just X?
Pierre-Marie Pédrot (Feb 21 2024 at 13:39):Since you're posting in the Ltac2 channel, I guess you want to use an Ltac2 solution?
Pierre-Marie Pédrot (Feb 21 2024 at 13:39):The short answer to your question is yes, but
Pierre-Marie Pédrot (Feb 21 2024 at 13:44):IANM terms in a context as generated by the context command come annotated with their bound variables in the substitution, which are represented as different runtime objects. If you try to cast these to a constr it will fail.
Pierre-Marie Pédrot (Feb 21 2024 at 13:44):So you can in theory check that the bound variable context is empty.
Pierre-Marie Pédrot (Feb 21 2024 at 13:45):This is quite fragile and ugly, the alternative is to plug back the matched term into the context itself and check it is equal to the internal one.
Pierre-Marie Pédrot (Feb 21 2024 at 13:46):This is less efficient, though.
Valerii Huhnin (Feb 21 2024 at 14:54):Well, I am kind of interested in both Ltac1 and Ltac2. I am not sure what is the right place to discuss Ltac1 so I decided to put my question here. Does it work differently in Ltac1 by the way?
Gaëtan Gilbert (Feb 21 2024 at 14:56):what does IANM mean?
Last updated: Oct 12 2024 at 13:01 UTC