Shortcut instances for queries made by almost every declaration #
Two kinds of instance problem occur in nearly every declaration of this project, are answered by a search through general instances each time, and are not shared between declarations.
Coercions. Using a set or a subobject as a type, using an element of a subtype as an element of the ambient type, and writing
∞for a smoothness order each ask for a coercion. The answer is found through the chain of coercion classes. EachCoercionShortcutdefinition records the instance selected for its displayedCoeTquery when its body is elaborated, then registers that alias at high priority. The declarations are sequential, so a later capture can see earlier aliases. This capture order alone does not establish equality with all coercion queries in an environment preceding the complete shortcut set.Facts about
ℝ. Arithmetic onℝneeds thatℝhas characteristic zero, that addition and multiplication are monotone, that the operations are continuous. None of these is stated directly forℝ; each is derived from the ordered field or normed field structure after the search has tried the unrelated ways of proving such a fact. The instances ofRealShortcutstate them forℝitself. These 44 theorem aliases have proposition-valued targets; for a fixed target and its data parameters, proof irrelevance identifies their proof values. This does not assert that instance search follows an identical route for other queries with unknown data parameters.