Mathlib Map

Structures · Lean core

HAdd

The notation typeclass for heterogeneous addition. This enables the notation a + b : γ where a : α, b : β.

Defined in
Init.Prelude
Shape
3 explicit arguments · adds hAdd
Open in Mathlib docs

Extends0

Extends nothing: this is a root of the hierarchy.

Extended by1

Forgetful instances

Provided automatically by

Concrete types that are instances20

  • Char
  • String
  • String.Pos.Raw
  • OrderType
  • String.Slice
  • 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.