Interface

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

definition

legend

NotePhysicalLayer.interface

physical-layer

PhysicalLayer.interface (m : ℕ) : InterfaceOld

Show details

fun 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

NoteInterfaceOld.Value.observeAll

InterfaceOld.Value.observeAll {m : ℕ} (v : (PhysicalLayer.interface m).Value) : Option (Fin m → Bit)

Show details

fun {m} v => 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