coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Define a function using tactics without a type

From: ikdc <ikdc AT mit.edu>
To: Joachim Breitner <mail AT joachim-breitner.de>, coq-club AT inria.fr
Subject: Re: [Coq-Club] Define a function using tactics without a type
Date: Mon, 16 Apr 2018 18:00:50 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=ikdc AT mit.edu; spf=Pass smtp.mailfrom=ikdc AT mit.edu; spf=None smtp.helo=postmaster AT dmz-mailsec-scanner-4.mit.edu
Ironport-phdr: 9a23:uJ6x4hU/5uRtGMk2J5SxzSTSG2bV8LGtZVwlr6E/grcLSJyIuqrYYxCHt8tkgFKBZ4jH8fUM07OQ7/i7HzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba98IRmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmijoINyQh/W/KlMJwgqJVrhGvqRNxzIHbYp2aOvVlc6PBft4XX3ZNUtpfWiFDBI63cosBD/AGPeZdt4T9plgOogaiCgKxA+7vyzxIiWLq0qAh1uQhEB3G0BY+EN0TrXTZtdP4P7ocX+CyyanH1zTDb/VO1Df87ojIaBEhruuWUbJ+a8rcz1QkGQDdjliItIDoPCmZ2+AXv2SF7+dsT/+jhm4/pw1soTWj3Nogh4rNi44PyF3J9T91zJgrKdC4TkNwfMSqH4FKty6AMot7WsMiTH9suCY90rAJpJu7fSkTxJQi3RHfaviHc5OW7R3/TeqROit3i2hjeLK5mRmy61Gsx+LmWsmx0VZKsjBJncfRuXAQzxDT686HReVh/kq5xDqC1Brf5+VeLUwqlafXMYMtz74ompoWq0vDHyv2mEvsjK+Rc0Up4umo6+f6bbr6vZKcMo50ih3kPqswh8O/HPw0MhISUGiD5eS8yLrj8FXlT7VNl/06i7XWsJTHJcsAvaO5GA9U0oM76xmlFTum0dIYnWMGLF1fYh6HgZLpaBnyJ6XaCv60g1Wp2B1xyvHaOLD7SsHIJ3nHuLXmdL196ksZwhA+zMxZ6ogSBrxXZLr4XVa0v9jFBDc4NRa1yqDpEoZTzIQbDGOMDqTRZKLRvVSg4+MzZeSAedlG637GN/E56qu23jcCklgHcPzxhMpFWDWDBv1jZn6hTz/pi9YFH30Nu1tsSe32zlCOTGwKPirgb+cH/jg+TbmeI8LbXIn80rmAwGG2EoAEPjkbWGDJKm/hcsC/Y9lJaC+WJZQ4wDABR/2kQo4lzhyl8RTxwrxhI/CRpmsdtI6l2dRotbXe

On 04/16/2018 05:24 AM, Emilio Jesús Gallego Arias wrote:

Hi Joachim,

Joachim Breitner
<mail AT joachim-breitner.de>
writes:

Definition foo4. exact body. Defined.

Is there a way of doing so? I.e. a way of using tactics to define a
function without having to specify the type before?

IMHO this certainly deserves to open a feature request on github, and
shouldn't been too hard to do for 8.9.

E.

https://coq.inria.fr/distrib/current/refman/miscellaneous.html#hevea_default1159

Require Import Coq.derive.Derive.
Derive type SuchThat type As foo.
exact 3.
Defined.

[Coq-Club] Define a function using tactics without a type, Joachim Breitner, 04/14/2018
- Re: [Coq-Club] Define a function using tactics without a type, Gaëtan Gilbert, 04/14/2018
- Re: [Coq-Club] Define a function using tactics without a type, Emilio Jesús Gallego Arias, 04/16/2018
  - Re: [Coq-Club] Define a function using tactics without a type, ikdc, 04/17/2018
    - Re: [Coq-Club] Define a function using tactics without a type, Pierre Courtieu, 04/17/2018