# How to detect (non)implicit arguments in ltac

**URL:** <https://discourse.rocq-prover.org/t/how-to-detect-non-implicit-arguments-in-ltac/269>\
**Category:** Using Rocq\
**Created:** [April 19, 2019, 3:16pm UTC](https://discourse.rocq-prover.org/t/how-to-detect-non-implicit-arguments-in-ltac/269 "2019-04-19T15:16:14Z")\
**Posts on this page:** 7\
**Page:** 1

<div class="post-metadata">

**Author:** ![Matafou](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/matafou/32/18_2.png) [@Matafou](https://discourse.rocq-prover.org/u/Matafou)\
**Post date:** [April 19, 2019, 3:16pm UTC](https://discourse.rocq-prover.org/t/how-to-detect-non-implicit-arguments-in-ltac/269/1 "2019-04-19T15:16:14Z")

</div>

Hi,

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

---

<div class="post-metadata">

**Author:** ![JasonGross](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/jasongross/32/32_2.png) [@JasonGross](https://discourse.rocq-prover.org/u/JasonGross)\
**Post date:** [April 19, 2019, 6:39pm UTC](https://discourse.rocq-prover.org/t/how-to-detect-non-implicit-arguments-in-ltac/269/2 "2019-04-19T18:39:11Z")

</div>

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).

---

<div class="post-metadata">

**Author:** ![Matafou](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/matafou/32/18_2.png) [@Matafou](https://discourse.rocq-prover.org/u/Matafou)\
**Post date:** [April 20, 2019, 8:31am UTC](https://discourse.rocq-prover.org/t/how-to-detect-non-implicit-arguments-in-ltac/269/3 "2019-04-20T08:31:05Z")

</div>

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?

---

<div class="post-metadata">

**Author:** ![JasonGross](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/jasongross/32/32_2.png) [@JasonGross](https://discourse.rocq-prover.org/u/JasonGross)\
**Post date:** [April 20, 2019, 3:28pm UTC](https://discourse.rocq-prover.org/t/how-to-detect-non-implicit-arguments-in-ltac/269/4 "2019-04-20T15:28:22Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![Matafou](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/matafou/32/18_2.png) [@Matafou](https://discourse.rocq-prover.org/u/Matafou)\
**Post date:** [May 6, 2019, 2:35pm UTC](https://discourse.rocq-prover.org/t/how-to-detect-non-implicit-arguments-in-ltac/269/5 "2019-05-06T14:35:46Z")

</div>

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:

```auto
    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

```

---

<div class="post-metadata">

**Author:** ![Zimmi48](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/zimmi48/32/7_2.png) [@Zimmi48](https://discourse.rocq-prover.org/u/Zimmi48)\
**Post date:** [May 7, 2019, 7:00am UTC](https://discourse.rocq-prover.org/t/how-to-detect-non-implicit-arguments-in-ltac/269/6 "2019-05-07T07:00:43Z")

</div>

Did you really mean `constr:(10%nat)` and not `constr:(11%nat)` on the last line of your first `match`?

---

<div class="post-metadata">

**Author:** ![Matafou](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/matafou/32/18_2.png) [@Matafou](https://discourse.rocq-prover.org/u/Matafou)\
**Post date:** [May 7, 2019, 7:26am UTC](https://discourse.rocq-prover.org/t/how-to-detect-non-implicit-arguments-in-ltac/269/7 "2019-05-07T07:26:36Z")

</div>

You are right it is an 11 there. Thanks!