coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Pierre Courtieu <Pierre.Courtieu AT cnam.fr>
To: Coq Club <coq-club AT inria.fr>
Cc: Joachim Breitner <mail AT joachim-breitner.de>
Subject: Re: [Coq-Club] Define a function using tactics without a type
Date: Tue, 17 Apr 2018 15:03:12 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-oi0-f53.google.com
Ironport-phdr: 9a23:6jYm8BPJ1eALWhJFqlsl6mtUPXoX/o7sNwtQ0KIMzox0Ivz8rarrMEGX3/hxlliBBdydt6ofzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxlGiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0vRz+s87lkRwPpiCcfNj427mfXitBrjKlGpB6tvgFzz5LIbI2QMvd1Y6HTcs4ARWdZXMlRWSxPDI2/YYUSEeQOIelWopLhp1sXtxayGRWgCP/txzJOm3T43bc60+MkEQzexgIgHswBsG7OrNrrKawfT+e1zLTSzTXfbvNZxyr945XPfx47oPGDQ6hwcdDPxkU1CQ7FiUiQqZb5PzOUyOsNrnOW4PZmVe21jm4rsQ9xoiK2y8oql4LHiIUVylXe+iV4xoY4Pdy4SEhhYd6lCpRcrS+aN5FwT8g/QG9ooD43xqMatZO/ZiQHy5QqywTBZ/CacIWE+BLuWeiXLDxlnnxqYqi/iAy38UW4yu3zSM200FFSoypAiNbMt3QN2wXU6siGVvdx50mh1DaB2gzJ5eFEJkc0laXfK5E/2LI/ip0TsUHbEi/3nkX5krOWe1069uS07+nreLbrq5+GO4Nqlw3zMb4il8yxDOggNwgBRWmb+eCy1L35+k35Ra1HjuU3kqbHqpDaP9oUqrSlDA9Sz4Yj8Qq/Dza439QFhnQHI1dFdwiGj4jtIV3BPPf4DfKnj1S2jDhr3+zGPqHmApjVMnfDl67hca9h5E5Y1Qo81stS54lUC7EEOPL8QFX9tN3eDh8jMgy72fzrCNtn1tBWZWXaKaiAeIjWrFXAsukoOqyHYJIfkDf7MfksofD02ywXg1gYKJGo0IENZTiTGel8P0SUfDK4utYMC30H+CE5Ufb2iVCfeTVVbnP0UbhqtWJzM56vEYqWHtPlu7eGxiruW8QOPjkXWGDJKm/hcsC/Y9lJbSuTJsF7lTldDOquToYg0VelswqokuM7fNqRwTURsNfY7PYw//fazEhg+jl9DsDb2GaIHTktwzE4AgQu1aU6mnRTj1eO1a8i3q5dHN1XovRICkI0aMWawOt9BNT/HAnGe4XRRQ==

nice!
P.

2018-04-17 0:00 GMT+02:00 ikdc
<ikdc AT mit.edu>:
> 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