Clément Blaudeau (Dec 30 2021 at 16:47): 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), ...).
Li-yao (Dec 30 2021 at 16:51):It's called Implicit Type(s)
Li-yao (Dec 30 2021 at 16:51):It's a great feature!
Clément Blaudeau (Dec 30 2021 at 17:03):Thanks ! I missed it reading through the documentation !
Notification Bot (Dec 30 2021 at 17:03):Clément Blaudeau has marked this topic as resolved.
Last updated: Oct 05 2023 at 02:01 UTC