Interface

Difficulty: easy — 2 definitions, 0 abbreviations, 0 lemmas, 0 theorems, 0 examples.

definition
legend
physical-layer
def PhysicalLayer.interface (m : ℕ) : InterfaceOld
Show details 
| PhysicalLayer.interface m = InterfaceOld.homogeneous Bit m

Complexity: 11 (size of the value term)

Outer dependencies: InterfaceOld

Inner dependencies: Bit, InterfaceOld.homogeneous, instNormBit

Lean core dependencies: Nat

Used by: DataLinkLayer.physical, InterfaceOld.Value.observeAll, NetworkArchitecture.physical

def InterfaceOld.Value.observeAll {m : ℕ} (v : (PhysicalLayer.interface m).Value) : Option (Fin m → Bit)
Show details 
| v.observeAll = if h : v.fired = Finset.univ then some fun p => v.value ⟨p, ⋯⟩ else none

Complexity: 245 (size of the value term)

Outer dependencies: Bit, InterfaceOld.Value, PhysicalLayer.interface

Mathlib dependencies: Finset, Finset.mem_univ, Finset.univ

Lean core dependencies: Eq, Eq.symm, Fin, Nat, Not, Option, dite

Used by: DataLinkLayer.physical

Dependency diagram

Drag to pan, Ctrl+scroll (or Cmd+scroll, or pinch on a touch screen) to zoom, click a node to jump to it.

definitiondeclared elsewheredependencyproof dependency
legend