structure Data.Unique : Type

A globally unique identifier, allocated via newUnique.

$$\text{Unique} \cong \mathbb{N}$$

Two Unique values are equal iff they were produced by the same call to newUnique.

• id : Nat

  The underlying identifier.

def Data.instBEqUnique.beq : Unique → Unique → Bool

Equations

• Data.instBEqUnique.beq { id := a } { id := b } = (a == b)
• Data.instBEqUnique.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Data.instBEqUnique : BEq Unique

Equations

• Data.instBEqUnique = { beq := Data.instBEqUnique.beq }

@[implicit_reducible]

instance Data.instHashableUnique : Hashable Unique

Equations

• Data.instHashableUnique = { hash := Data.instHashableUnique.hash }

def Data.instHashableUnique.hash : Unique → UInt64

Equations

• Data.instHashableUnique.hash { id := a } = mixHash 0 (hash a)

@[implicit_reducible]

instance Data.instReprUnique : Repr Unique

Equations

• Data.instReprUnique = { reprPrec := Data.instReprUnique.repr }

def Data.instReprUnique.repr : Unique → Nat → Std.Format

Equations

• Data.instReprUnique.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "id" ++ Std.Format.text " := " ++ (Std.Format.nest 6 (repr x✝.id)).group) " }"

@[implicit_reducible]

instance Data.instOrdUnique : Ord Unique

Equations

• Data.instOrdUnique = { compare := fun (a b : Data.Unique) => compare a.id b.id }

@[implicit_reducible]

instance Data.instToStringUnique : ToString Unique

Equations

• Data.instToStringUnique = { toString := fun (u : Data.Unique) => toString "Unique(" ++ toString u.id ++ toString ")" }

def Data.newUnique : IO Unique

Allocate a fresh Unique value. Each call returns a distinct value.

$$\text{newUnique} : \text{IO}(\text{Unique})$$

Equations

• Data.newUnique = do let n ← ST.Ref.get Data.uniqueCounter✝ ST.Ref.set Data.uniqueCounter✝ (n + 1) pure { id := n }

@[inline]

def Data.Unique.hashUnique (u : Unique) : Nat

Extract the underlying Nat from a Unique.

Equations

• u.hashUnique = u.id