Theorems · Inductive type · logic and foundations

Fact

Prop → Prop

Wrapper for adding elementary propositions to the type class systems. Warning: this can easily be abused. See the rest of this docstring for details. Certain propositions should not be treated as a class globally, but sometimes it is very convenient to be able to use the type class system in specific circumstances. For example, ZMod p is a field if and only if p is a prime number. In order to be able to find this field instance automatically by type class search, we have to turn p.Prime into an instance implicit assumption. On the other hand, making Nat.Prime a class would require a major refactoring of the library, and it is questionable whether making Nat.Prime a class is desirable at all. The compromise is to add the assumption [Fact p.Prime] to ZMod.instField. In particular, this class is not intended for turning the type class system into an automated theorem prover for first-order logic.

Defined in

Mathlib.Logic.Basic

Cited by

2,726 results in Mathlib

Foundations

Depth 0 from the axioms, rests on 1 definitions · uses no axioms