Interface

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

definition
legend
data-link-layer
DataLinkLayer.interface (poly : List Bool) (n : ℕ) : InterfaceOld
Show details 
fun poly n => InterfaceOld.single (Frame poly n poly.length)

Complexity: 37 (size of the value term)

Outer dependencies: InterfaceOld

Inner dependencies: Frame, InterfaceOld.single, instNonemptyFrame, instNormFrame

Lean core dependencies: Bool, List, List.length, Nat

Used by: DataLinkLayer.network, DataLinkLayer.physical, NetworkArchitecture.dataLink, NetworkArchitecture.stack

DataLinkLayer.physical (poly : List Bool) (n : ℕ) :
  Layer (PhysicalLayer.interface (n + poly.length)) (DataLinkLayer.interface poly n)
Show details 
fun poly n v =>
  match v.left.observeAll, v.right.observe with
  | none, none => True
  | some bits, some e => bits = Fin.append e.payload e.check
  | x, x_1 => False

Complexity: 369 (size of the value term)

Outer dependencies: DataLinkLayer.interface, Layer, PhysicalLayer.interface

Inner dependencies: Bit, Frame, InterfaceOld.Value, InterfaceOld.Value.left, InterfaceOld.Value.observe, InterfaceOld.Value.observeAll, InterfaceOld.Value.right, InterfaceOld.tensor, instNormFrame

Mathlib dependencies: Fin.append

Lean core dependencies: Bool, Eq, False, Fin, List, List.length, Nat, Nat.hasNotBit, Nat.land, Nat.ne_of_beq_eq_false, Nat.shiftRight, Option, True, Unit, Unit.unit

Used by: NetworkArchitecture.stack

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