coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] implicit arguments

From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] implicit arguments
Date: Thu, 10 Dec 2020 14:46:21 +1100
Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=anu.edu.au; dmarc=pass action=none header.from=anu.edu.au; dkim=pass header.d=anu.edu.au; arc=none
Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=tDgZ6TUTSg0m8XgZpTYZTm/C3RgI6g272NYnOCfzZ7k=; b=Ig1lLERpK1eoUoGxaNmdpLUW97HrHtcXcG1XDN25zIR5xw7q51dp8uQR9yIcYLmScA8SNL10qWoysy0pwn0o+Pk0s4jpO/yTAxLXA96Cwkl9+izymSFdwYpZohLDUPFSL0pLd91nXoEfHF+qNRLifAYVNwUOyRl6AHd8LFSHh8IWCTWyeV0xfkdnK3CVm1SS+OhFq15bHO/Ho3TObyXh7EazlXUOJv9IygOGRnoX67n4mREshp1CyDuZXQ4Qb+8vCOy/cqu9Iejc9K3SMZDvrvee/nyHf9Gh3zpxragBwDcCHx1rDdInN03swuYArW94Mtmu2SLtl0eh4WRPBgNcEw==
Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=PZ/CAofhH+nknrvI0D0WMHihMgAA7MNahEYe8txTUrWvJRaYktTZ/tHRJby/xsTl/e051QZvLhXtY1Hc32FbAo4ZF1hm+1//2HtbAP48TjTw/WWiwdvRJcK5wltA3u4KrHPiKMPSuKR+Ooi4gsFuEYez94sp46lFI5BCYbY7B3sSPXAbHJhkUHrwLmtp+B98U+DmmM4Bzq98Su1qfJTHlSzThY/FWuqv95tdHH+xOkRCQxbgdyKi2yLETioL2BMpIa22EOEQgzVIW+OhqKGuswjU8Fp+T0TrRiDCACJVwXPvgDQE5LS2d3DaC19jBbxzKG+JB42DOF+UGhAn9+N6Dw==
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.mailfrom=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.helo=postmaster AT AUS01-ME3-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:6wZLqBXoSUBrcscZdafjiqf6JS7V8LGtZVwlr6E/grcLSJyIuqrYbRWFt8tkgFKBZ4jH8fUM07OQ7/m/HzVfsN3b4TgrS99lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUhrwOhBoKevrB4Xck9q41/yo+53Ufg5EmCexbal9IRmrrwjdrNQajIlmJ6o+1BfEpmZDdvhLy29vOV+dhQv36N2q/J5k/SRQuvYh+NBFXK7nYak2TqFWASo/PWwt68LlqRfMTQ2U5nsBSWoWiQZHAxLE7B7hQJj8tDbxu/dn1ymbOc32Sq00WSin4qx2RhLklDsLOjgk+2zRl8d+jr9UoAi5qhJhw4DafYKbOvRwcazBct0aRGVOU91NVyFDGI6wc5cDAuQDMOtesoLzp0EOrRy7BQS0AO3g1CVIiWHz3aw6zu8vHxvJ3QI7H9IJtnTfsdL4OqMMXuCv0qbIyDXCY+lY1zjn5onIaRchofeXUL1qd8rR1FMjGB3YgVWNs4DqJS6V2/0LvmOG4OVuSfihhHQ7qwFtvDev3MEsh5HVi48bxV7K9Sp3zJooKdO3RkN1YcKoHZhfuiyVM4Z7XN0uT3xqtSsmxLMKpYK2cSoOxZk5wxPSb+GKfomJ7xzsUuuaPDR2hGp9db+wmxq+61WsxvH+W8WuzVpGsilInsPIu30OzxDe5cyKRuFg8kqixTqDzQDe5+5eLUwqiabXNZgsyaMqmJUJq0TMBCr2lV32jKCIckUk/fCl5vjpbbv7upOQKpZ4hAbxPKkgg8C/Bv83PRYUU2ic5OS8yKbs/UrkQLVMk/I6iLHZsIrdJcQHuKG2HxNV0ock6xa5FTum18kYnWUDLFJCfxKHjJLlNE3JIPD9Ffu/glKsnyl3x/3eMbDtHo/BImXfnLrjZ7px9lJQxQkpwd1b5J9YErQBL+jyWk/1utzYFBg5MwmszujjFtp9zJ0RWWePA6ODPq3dq1GJ5vkoI+mKf4IaojD9K+U/6/HwkHA5hEURcrO03ZcPcnC3AuxmI1mFYXrrmtoODWAKvhMnQOP2jF2CTCVcam2pX6M84zE7EJipAZ3CRoCrmryB3T20EodYZmBcWRiwFiKifIKdHvwIdSi6I8l7kzVCW6LrA9sq0gjrvwvnwZJmKPDV82sWr8Sw+sJy4rjxmAs/8C08I82CyGaLBzVWk3kFQi5w8Klgukt74l6FzO51j+EeHMEFtKABaRszKZOJl78yMNv1QA+UJo7YGmbjec2vBHQKdvx0xtYPZ0hnHND71ELK2TfsDrMI0bWWVsVtrvDsmkPpLsM48E7okbE7hgB8EMJJKCurirM5/hWBX9eUwXXcrL6jcOEn5ACI9GqHyjbR7mhla1YpFIDoBjUYbEaQqsnl7ETfSbPoEa4gLgZK1c+FLO1Nd8HtilJFAvzkPYaHbg==

Hi,

I have tried to find out when implicit arguments are inserted. Is this in the documentation anywhere?

With a function

lja_dd_ord < About no_rpt_same.
no_rpt_same :
forall U : Type,
relationT U ->
forall (rules : list U -> U -> Type) (prems : U -> Type) (c0 : U),
derrec rules prems c0 -> Type

Arguments U, rules, prems, c0 are implicit

I find

lja_dd_ord < Check no_rpt_same seq_ord.
no_rpt_same seq_ord
: forall (rules : list (srseq (PropF ?V)) -> srseq (PropF ?V) -> Type)
(prems0 : srseq (PropF ?V) -> Type) (c0 : srseq (PropF ?V)),
derrec rules prems0 c0 -> Type

which is as I expected (as a matter of fact, I can't find this documented either, but I've discovered from experience that implicit arguments (non-maximal) are inserted up to the last explicit argument)

but

lja_dd_ord < Check no_rpt_same seq_ord (prems:=prems).
no_rpt_same seq_ord (prems:=prems)
: forall c0 : srseq (PropF V), derrec ?rules prems c0 -> Type

ie it seems to have inserted the implicit argument rules also.

What are the rules about this?

And if there are any tips for finding things like this in the documentation, I'd appreciate it. For example, the symbol := isn't in the general index, which I would have expected.

Thanks

Jeremy

[Coq-Club] implicit arguments, Jeremy Dawson, 12/10/2020
- Re: [Coq-Club] implicit arguments, Jim Fehrle, 12/10/2020
  - Re: [Coq-Club] implicit arguments, Jeremy Dawson, 12/12/2020
    - Re: [Coq-Club] implicit arguments, Jim Fehrle, 12/13/2020
    - Re: [Coq-Club] implicit arguments, Fabian Kunze, 12/13/2020
      - Re: [Coq-Club] implicit arguments, Jeremy Dawson, 12/13/2020