Stream: Coq users

Topic: ✔ Need for comma in `Arguments` command?

view this post on Zulip Julin S (Dec 01 2021 at 15:58):

I was looking at the definition of sum at

Inductive sum (A B:Type) : Type :=
  | inl : A -> sum A B
  | inr : B -> sum A B.

(* Why the comma here? *)
Arguments inl {A B} _ , [A] B _.
Arguments inr {A B} _ , A [B] _.

What does the comma in the Argument commands mean?

Arguments inl {A B} _ means that A and B are maximally inserted implicit arguments (right?), but what does the [A] B _ coming after mean? Is it making some sort of 'correction' (I guess not) saying that A is now non-maximally inserted implicit and that B is no longer implicit?

I also couldn't figure out why the _ that comes at the end was needed. Why is that needed?

I had a glance at but couldn't find if what I was looking for is mentioned there.

view this post on Zulip Yannick Forster (Dec 01 2021 at 16:02):

It adds a second possible way of interpreting arguments. Maybe an example is best:

Check (inl nat true).
Check (inl true).

Arguments inl {A B} _.
Fail Check (inl nat true).

view this post on Zulip Gaëtan Gilbert (Dec 01 2021 at 16:04):


Print Implicit inl.
inl : forall {A B : Type}, A -> A + B

When applied to no more than 1 argument:
  Arguments A, B are implicit and maximally inserted
When applied to 2 arguments:
  Argument A is implicit

view this post on Zulip Paolo Giarrusso (Dec 01 2021 at 20:04):

TIL! And it’s even documented!

view this post on Zulip Julin S (Dec 02 2021 at 05:31):

Thanks! So it's like

Check inl nat true. (* [A] B _ *)
Check inl true.     (* {A B} _ *)

view this post on Zulip Julin S (Dec 02 2021 at 05:32):

Also found the need for the underscore at the end. It's for the value itself (right?). Like

Check (@inl nat bool 3).
(* inl 3 : nat + bool *)

Check (@inr nat bool true).
(* inr true : nat + bool *)

view this post on Zulip Notification Bot (Dec 02 2021 at 05:32):

Ju-sh has marked this topic as resolved.

Last updated: Jun 18 2024 at 00:02 UTC