coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Joachim Breitner <mail AT joachim-breitner.de>
To: coq-club AT inria.fr
Subject: [Coq-Club] Define a function using tactics without a type
Date: Fri, 13 Apr 2018 16:41:38 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mail AT joachim-breitner.de; spf=Neutral smtp.mailfrom=mail AT joachim-breitner.de; spf=None smtp.helo=postmaster AT hermes.serverama.de
Ironport-phdr: 9a23:s+tKdBQejWxZLJ17VhES8S0xwdpsv+yvbD5Q0YIujvd0So/mwa69YxWN2/xhgRfzUJnB7Loc0qyK6/umATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfb1/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4qF2QxHqlSgHLSY0/mLKhMJwkqxVrg6uqRtwzIPPb4GZKOBzc7nHcN8GR2dMWNtaWSxbAoO7aosCF+4PPeFCoIbhp1sOrB6+DhSxCeP11DBIh2P23ask3OQ7DArL2wkgEMgPsHTQt9j1NqASXvqpw6nIzDXDaupa1izn6IfWcxAhvfeMUqxqccbL1EYgCRrIg1ONooLrODOV0/4Cs2md7+d4V+KvjHQopB1xojiuw8cgk5LGhpgLxVDF6SV5xpg6JceiREFmf9GpFoZbuSKCN4ZuX88vQWBltDw+x7Ecp5K3YSYHxI46yxPRZfGKdZWD7Aj5W+aLOzh4gWpoeLKhiBa29kit0u38Wdeu0FZPsCVFicPAtmsT2BzJ9MiIVOF98V2k2TmVzQzc9/9LLVg1lardNZEh3qY9mocRvEnCBCP7nF/6gLGLekgq4OSk9urqb7v+qp+ZLYB0iwX+Mqo0msy4BOQ1Kg0OUHKa+eS4z7Dj/0r5T69Wgf02k6nZtYnWKt8BpqGnAg9VzoAj5AilDzu8zdsXg2ELLEhZdxKfk4jpJ1bOLejkAve4mlSgiStkx/TbPrL6GZjNNXjCkLL5fbln8UJcyQwzzcpe551OEL0BLujzCQfNs4nTCQZ8OAipyc7mDs9838UQQzGhGKicZYHVuFSI5+dnCfOBZZMTtSy1f/0s5vrGj3gwkl8ceOyjx5YWdHa1BLJqLhPKMjLXnt4dHDJS7UIFR+vwhQjaCG8BVzOJR6s5owoDJsejBIbHSJqqhebYjiW8F5ZWZ2UDAEqBEGvuep/CV/peMnvOcP8kqSQNUP2ac6FkzQun7laoyb1uJerV/2gSr5/iyN54/avfmENqrGEmP4Gmy2iIClpMsCYISjsxhvktoUFnz1qYl7N1meJVD9VW7rVFX1ViOA==

Hi,

I can write

Definition foo1 : type := body.
Definition foo2 := body.
Definition foo3 : type. exact body. Defined.

but it seems I cannot write

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?

What I do now is something like this

Definition foo4_type : Type.
let ty := type of body in exact ty. Defined.
Definition foo4 : foo4_type exact body. Defined.

but it is a bit clunky.

(The actual tactic is a bit larger and does some interesting stuff
before calling [exact]; namely; getting the body of a local let out of
a complex function).

Thanks,
Joachim

--
Joachim “nomeata” Breitner

mail AT joachim-breitner.de
https://www.joachim-breitner.de/

Attachment: signature.asc
Description: This is a digitally signed message part

[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