pith. machine review for the scientific record. sign in
def definition def or abbrev

grayInverse

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  38def grayInverse (g : ℕ) : ℕ :=

proof body

Definition body.

  39  let rec loop (shift : ℕ) (acc : ℕ) (fuel : ℕ) : ℕ :=
  40    match fuel with
  41    | 0 => acc
  42    | fuel' + 1 =>
  43      let shifted := g >>> shift
  44      if shifted = 0 then acc
  45      else loop (shift + 1) (acc ^^^ shifted) fuel'
  46  loop 0 0 64
  47
  48/-- Hypothesis envelope for Gray code classical properties. -/

used by (5)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.