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

pattern3

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)

  82def pattern3 : Fin 8 → Pattern 3
  83| ⟨0, _⟩ => fun _ => false
  84| ⟨1, _⟩ => fun j => decide (j.val = 0)
  85| ⟨2, _⟩ => fun j => decide (j.val = 1)
  86| ⟨3, _⟩ => fun j => decide (j.val = 0 ∨ j.val = 1)
  87| ⟨4, _⟩ => fun j => decide (j.val = 2)
  88| ⟨5, _⟩ => fun j => decide (j.val = 0 ∨ j.val = 2)
  89| ⟨6, _⟩ => fun j => decide (j.val = 1 ∨ j.val = 2)
  90| ⟨7, _⟩ => fun _ => true
  91
  92/-- Canonical 3-bit Gray order as a function `Fin 8 → Fin 8`.
  93
  94Sequence: [0,1,3,2,6,7,5,4]. -/

used by (4)

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

depends on (5)

Lean names referenced from this declaration's body.