Subtypes #
These are ported from the Lean 3 standard library file init/data/subtype/basic.lean
.
If there is some element satisfying the predicate, then the subtype is inhabited.
Equations
- Subtype.inhabited h = { default := { val := a, property := h } }