Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • From: e AT x80.org (Emilio Jesús Gallego Arias)
  • To: Joachim Breitner <mail AT joachim-breitner.de>
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Define a function using tactics without a type
  • Date: Mon, 16 Apr 2018 11:24:21 +0200
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=e AT x80.org; spf=Pass smtp.mailfrom=e AT x80.org; spf=Pass smtp.helo=postmaster AT x80.org
  • Ironport-phdr: 9a23:0pmbVhZv152rFirSuQSg9Q3/LSx+4OfEezUN459isYplN5qZoM2+bnLW6fgltlLVR4KTs6sC17KN9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCazbL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD0fOjA57m/Zl8twjKxVrh2jpBJwzYHbb52OOfpiYq/QZ88WSXZbU8tTUSFKH4Oyb5EID+oEJetXsZLwplQNoBeiHwWsA/nvyjBVjXPy0qM61uUhEQXH3AwnAtkAtGrbrM7vLKcJTOu7zbPHzTHHb/xI1jf975XDfww7ofGNR71was/dxE8yHA3GllWdsZHpMjCW2+gXrWSX8ettWfiyh2Mltg19uCWjy8kyhoXRm44Yzl7J+T9nzIs1ONG0Uk92bNC+HJZesyyXMZZ9TNk4TGFyoik6z6ULuZ6lcygOz5Qq3xHeZv+bf4SS5RLjTumRLS95hHJjZr2/mw6//VWjx+D/TMW4zkhGoytfntXRtH0Bygbf5tWJR/dj5kuh3CyA1wHX6uFKO0A0kq/bJoY/zbMrmZsesljPEjXxmEXsg6+abl8k9fSw6+T7frXmoYeROJNzigHnK6ghhsi/AfkjPQUVRGia+eG81KX58kHjQbVKiOc2kqjDv5zAK8QbvP3xPwgA8IEq4Ba+Cn+MytkZgX8KNhoRfRuGi6DrPFjFIPH9SP2ljlWwljpxgfzLaO7PGJLIe3XrgOe5O7Fn5AYc5Q8yydFYr7BZESMaaN36Xkv8u9uQJwU4Ohf1kLWvM8l0yo5LATHHOaSeKq6H6QbZtNJqGPGFYcougBi4LvEk4/D0inpoy09NJe+ux5RFMSnkTMQjGF2QZD/XuvlECX0D71guHLSsj0eNA2YKOiSCGpkk7zR+M7qISIfOQof80qzRhGG8BJIEP20=
  • Organization: X80 Heavy Industries

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.



Archive powered by MHonArc 2.6.18.

Top of Page