I was looking at the definition of `sum`

at https://coq.inria.fr/library/Coq.Init.Datatypes.html

```
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 https://coq.inria.fr/refman/language/extensions/implicit-arguments.html but couldn't find if what I was looking for is mentioned there.

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

also

```
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
*)
```

TIL! And it’s even documented! https://coq.inria.fr/refman/language/extensions/arguments-command.html#coq:cmd.Arguments.

Thanks! So it's like

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

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 *)
```

Ju-sh has marked this topic as resolved.

Last updated: Jun 18 2024 at 00:02 UTC