Stream: Coq users

Topic: ✔ Default type for a variable name


view this post on Zulip Clément Blaudeau (Dec 30 2021 at 16:47):

Is there a way to say to Coq "when you cannot infer the type of a variable named SomeName, assume it's SomeType". I don't want it as a parameter (or variable). I was hoping for something like Default Type SomeName : SomeType. In all my development, SomeName always has the same type, it's just that it cannot always be inferred.
Side style question : I need this because I write my theorems without type information on my quantifiers (forall a b c, ...). Is it bad practice ? Should I add all the type info everywhere? (forall (a:A) (b:B) (c:C), ...).

view this post on Zulip Li-yao (Dec 30 2021 at 16:51):

It's called Implicit Type(s)

view this post on Zulip Li-yao (Dec 30 2021 at 16:51):

It's a great feature!

view this post on Zulip Clément Blaudeau (Dec 30 2021 at 17:03):

Thanks ! I missed it reading through the documentation !

view this post on Zulip Notification Bot (Dec 30 2021 at 17:03):

Clément Blaudeau has marked this topic as resolved.


Last updated: Jan 29 2023 at 01:02 UTC