def NatPair.pair (n m : ℕ) : ℕ

Equations

• NatPair.pair n m = 2 ^ n * (m * 2 + 1) - 1

@[irreducible]

def NatPair.fst (r : ℕ) : ℕ

Equations

• NatPair.fst r = if h : Even r then 0 else 1 + NatPair.fst (r / 2)

def NatPair.snd (r : ℕ) : ℕ

Equations

• NatPair.snd r = ((r + 1) / 2 ^ NatPair.fst r - 1) / 2

def NatPair.f (p : ℕ × ℕ) : ℕ

Equations

• NatPair.f p = NatPair.pair p.1 p.2

def NatPair.g (r : ℕ) : ℕ × ℕ

Equations

• NatPair.g r = (NatPair.fst r, NatPair.snd r)