Structures · Lean core
HSub
The notation typeclass for heterogeneous subtraction.
This enables the notation a - b : γ where a : α, b : β.
- Defined in
- Init.Prelude
- Shape
- 3 explicit arguments · adds hSub
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances16
- String.Pos.Raw
- Std.Time.Week.Offset
- Std.Time.Second.Offset
- Std.Time.Minute.Offset
- Std.Time.Nanosecond.Offset
- Std.Time.Day.Offset
- Std.Time.Hour.Offset
- Std.Time.Millisecond.Offset
- Std.Time.Duration
- Std.Time.Timestamp
- Std.Time.WallTime
- Aesop.SlotIndex
- Std.Time.PlainDateTime
- Std.Time.PlainDate
- Std.Time.PlainTime
- Std.Time.DateTime
How is a type an instance?
Loading the hierarchy index…
Assumed by0
No theorem or definition in Mathlib takes this class as a hypothesis.
Ancestors0
No ancestors.