Julin S (Dec 01 2021 at 15:58): Julin S (Dec 01 2021 at 15:58):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.
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).
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.
Julin S (Dec 02 2021 at 05:31):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: Sep 30 2023 at 07:01 UTC