Subtype.{u} {α : Sort u} (p : α → Prop)
    : Sort (max 1 u)

Subtype p, usually written as {x : α // p x}, is a type which represents all the elements x : α for which p x is true. It is structurally a pair-like type, so if you have x : α and h : p x then ⟨x, h⟩ : {x // p x}. An element s : {x // p x} will coerce to α but you can also make it explicit using s.1 or s.val.

Constructor

Subtype.mk.{u} {α : Sort u} {p : α → Prop} (val : α) (property : p val) : Subtype p

Fields

property	:	p self.val
		If s : {x // p x} then s.2 or s.property is the assertion that p s.1, that is, that s is in fact an element for which p holds.
val	:	α
		If s : {x // p x} then s.val : α is the underlying element in the base type. You can also write this as s.1, or simply as s when the type is known from context.