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), ...).
It's a great feature!
Thanks ! I missed it reading through the documentation !
Clément Blaudeau has marked this topic as resolved.
Last updated: Jan 29 2023 at 01:02 UTC