Hi,

I would like to extract the non implicit arguments of an application in ltac. Is it possible?

Hi,

I would like to extract the non implicit arguments of an application in ltac. Is it possible?

1 Like

I believe it is not possible. I believe implicit status is very early in the pipeline, and by the time you have constrs (or even uconstrs), it is no longer present.

You can extract non-dependent arguments; or arguments that would not be made implicit by `Set Implicit Arguments`

(both of these by parsing the type).

1 Like

Hi Jason, I am interested in extracting the arguments that would be mage implicit by imlicit arguments. How do you do that please? by checking occurrences of variables in types?

Yeah, you basically need to reimplement the algorithm of `Set Implicit Arguments`

in Ltac

For the record I ended up with a very stupid (but quite efficient) hack to detect the number of *head* implicit arguments. I will maybe try something smarter but this fits my needs for now:

```
lazymatch th with
| (?z ?a ?b ?c ?d ?e ?f ?g ?h ?i ?j ?k) =>
match th with
| _ => let foo := constr:(z _ _ _ _ _ _ _ _ _ _ k) in constr:(1%nat)
| _ => let foo := constr:(z _ _ _ _ _ _ _ _ _ j k) in constr:(2%nat)
| _ => let foo := constr:(z _ _ _ _ _ _ _ _ i j k) in constr:(3%nat)
| _ => let foo := constr:(z _ _ _ _ _ _ _ h i j k) in constr:(4%nat)
| _ => let foo := constr:(z _ _ _ _ _ _ g h i j k) in constr:(5%nat)
| _ => let foo := constr:(z _ _ _ _ _ f g h i j k) in constr:(6%nat)
| _ => let foo := constr:(z _ _ _ _ e f g h i j k) in constr:(7%nat)
| _ => let foo := constr:(z _ _ _ d e f g h i j k) in constr:(8%nat)
| _ => let foo := constr:(z _ _ c d e f g h i j k) in constr:(9%nat)
| _ => let foo := constr:(z _ b c d e f g h i j k) in constr:(10%nat)
| _ => let foo := constr:(z a b c d e f g h i j k) in constr:(10%nat)
end
| (?z ?b ?c ?d ?e ?f ?g ?h ?i ?j ?k) =>
match th with
| _ => let foo := constr:(z _ _ _ _ _ _ _ _ _ k) in constr:(1%nat)
| _ => let foo := constr:(z _ _ _ _ _ _ _ _ j k) in constr:(2%nat)
| _ => let foo := constr:(z _ _ _ _ _ _ _ i j k) in constr:(3%nat)
| _ => let foo := constr:(z _ _ _ _ _ _ h i j k) in constr:(4%nat)
| _ => let foo := constr:(z _ _ _ _ _ g h i j k) in constr:(5%nat)
| _ => let foo := constr:(z _ _ _ _ f g h i j k) in constr:(6%nat)
| _ => let foo := constr:(z _ _ _ e f g h i j k) in constr:(7%nat)
| _ => let foo := constr:(z _ _ d e f g h i j k) in constr:(8%nat)
| _ => let foo := constr:(z _ c d e f g h i j k) in constr:(9%nat)
| _ => let foo := constr:(z b c d e f g h i j k) in constr:(10%nat)
end
| (?z ?c ?d ?e ?f ?g ?h ?i ?j ?k) =>
match th with
| _ => let foo := constr:(z _ _ _ _ _ _ _ _ k) in constr:(1%nat)
| _ => let foo := constr:(z _ _ _ _ _ _ _ j k) in constr:(2%nat)
| _ => let foo := constr:(z _ _ _ _ _ _ i j k) in constr:(3%nat)
| _ => let foo := constr:(z _ _ _ _ _ h i j k) in constr:(4%nat)
| _ => let foo := constr:(z _ _ _ _ g h i j k) in constr:(5%nat)
| _ => let foo := constr:(z _ _ _ f g h i j k) in constr:(6%nat)
| _ => let foo := constr:(z _ _ e f g h i j k) in constr:(7%nat)
| _ => let foo := constr:(z _ d e f g h i j k) in constr:(8%nat)
| _ => let foo := constr:(z c d e f g h i j k) in constr:(9%nat)
end
| (?z ?d ?e ?f ?g ?h ?i ?j ?k) =>
match th with
| _ => let foo := constr:(z _ _ _ _ _ _ _ k) in constr:(1%nat)
| _ => let foo := constr:(z _ _ _ _ _ _ j k) in constr:(2%nat)
| _ => let foo := constr:(z _ _ _ _ _ i j k) in constr:(3%nat)
| _ => let foo := constr:(z _ _ _ _ h i j k) in constr:(4%nat)
| _ => let foo := constr:(z _ _ _ g h i j k) in constr:(5%nat)
| _ => let foo := constr:(z _ _ f g h i j k) in constr:(6%nat)
| _ => let foo := constr:(z _ e f g h i j k) in constr:(7%nat)
| _ => let foo := constr:(z d e f g h i j k) in constr:(8%nat)
end
| (?z ?e ?f ?g ?h ?i ?j ?k) =>
match th with
| _ => let foo := constr:(z _ _ _ _ _ _ k) in constr:(1%nat)
| _ => let foo := constr:(z _ _ _ _ _ j k) in constr:(2%nat)
| _ => let foo := constr:(z _ _ _ _ i j k) in constr:(3%nat)
| _ => let foo := constr:(z _ _ _ h i j k) in constr:(4%nat)
| _ => let foo := constr:(z _ _ g h i j k) in constr:(5%nat)
| _ => let foo := constr:(z _ f g h i j k) in constr:(6%nat)
| _ => let foo := constr:(z e f g h i j k) in constr:(7%nat)
end
| (?z ?f ?g ?h ?i ?j ?k) =>
match th with
| _ => let foo := constr:(z _ _ _ _ _ k) in constr:(1%nat)
| _ => let foo := constr:(z _ _ _ _ j k) in constr:(2%nat)
| _ => let foo := constr:(z _ _ _ i j k) in constr:(3%nat)
| _ => let foo := constr:(z _ _ h i j k) in constr:(4%nat)
| _ => let foo := constr:(z _ g h i j k) in constr:(5%nat)
| _ => let foo := constr:(z f g h i j k) in constr:(6%nat)
end
| (?z ?g ?h ?i ?j ?k) =>
match th with
| _ => let foo := constr:(z _ _ _ _ k) in constr:(1%nat)
| _ => let foo := constr:(z _ _ _ j k) in constr:(2%nat)
| _ => let foo := constr:(z _ _ i j k) in constr:(3%nat)
| _ => let foo := constr:(z _ h i j k) in constr:(4%nat)
| _ => let foo := constr:(z g h i j k) in constr:(5%nat)
end
| (?z ?h ?i ?j ?k) =>
match th with
| _ => let foo := constr:(z _ _ _ k) in constr:(1%nat)
| _ => let foo := constr:(z _ _ j k) in constr:(2%nat)
| _ => let foo := constr:(z _ i j k) in constr:(3%nat)
| _ => let foo := constr:(z h i j k) in constr:(4%nat)
end
| (?z ?i ?j ?k) =>
match th with
| _ => let foo := constr:(z _ _ k) in constr:(1%nat)
| _ => let foo := constr:(z _ j k) in constr:(2%nat)
| _ => let foo := constr:(z i j k) in constr:(3%nat)
end
| (?z ?j ?k) =>
match th with
| _ => let foo := constr:(z _ k) in constr:(1%nat)
| _ => let foo := constr:(z j k) in constr:(2%nat)
end
| (?z ?j) => constr:(1%nat)
| _ => constr:(0%nat)
end
```

Did you really mean `constr:(10%nat)`

and not `constr:(11%nat)`

on the last line of your first `match`

?

You are right it is an 11 there. Thanks!