Basic definitions

inductive Unicode.ByteOrder : Type

The order of the bytes of a code unit wider than a byte.

• big : ByteOrder

  Big-endian: the most significant byte first.

• little : ByteOrder

  Little-endian: the least significant byte first.

@[instance_reducible]

instance Unicode.instInhabitedByteOrder : Inhabited ByteOrder

Equations

• Unicode.instInhabitedByteOrder = { default := Unicode.instInhabitedByteOrder.default }

@[instance_reducible]

instance Unicode.instDecidableEqByteOrder : DecidableEq ByteOrder

Equations

• Unicode.instDecidableEqByteOrder x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Unicode.instReprByteOrder : Repr ByteOrder

Equations

• Unicode.instReprByteOrder = { reprPrec := Unicode.instReprByteOrder.repr }

def Unicode.instReprByteOrder.repr : ByteOrder → Nat → Std.Format

Equations

• Unicode.instReprByteOrder.repr Unicode.ByteOrder.big prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Unicode.ByteOrder.big")).group prec✝
• Unicode.instReprByteOrder.repr Unicode.ByteOrder.little prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Unicode.ByteOrder.little")).group prec✝