def
definition
def or abbrev
mortonIndex
show as:
view Lean formalization →
formal statement (Lean)
20def mortonIndex (x y z : Nat) : Nat :=
proof body
Definition body.
21 x + y * 1000 + z * 1000000
22
23/-- Octant level: how many octant subdivisions (0 = whole space, k = 8^k subregions). -/