Arp

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

definition
legend
AddressResolution (Address : Type) (k : ℕ) : Type
Show details 
| AddressResolution.mk : {Address : Type} → {k : ℕ} → (Address → Option (Fin k)) → AddressResolution Address k

Outer dependencies: (none)

Lean core dependencies: Eq, Fin, HEq, Nat, Option, SizeOf, eq_of_heq

Used by: NetworkLayer.resolves

NetworkLayer.resolves (Address : Type) [Nonempty Address] [Norm Address] {k : ℕ}
  (table : AddressResolution Address k) (poly : List Bool) (n : ℕ) :
  Layer (NetworkLayer.interface Address n) (DataLinkLayer.links poly n k)
Show details 
fun Address [Nonempty Address] [Norm Address] {k} table poly n v =>
  match v.left.observe with
  | none => v.right.fired = ∅
  | some p =>
    match table.resolve p.next with
    | none => v.right.fired = ∅
    | some link =>
      ∃ (h : link ∈ v.right.fired),
        v.right.fired = {link} ∧ (v.right.value ⟨link, h⟩).payload = p.payload

Complexity: 751 (size of the value term)

Outer dependencies: AddressResolution, DataLinkLayer.links, Layer, NetworkLayer.interface

Inner dependencies: Bit, BitSequence, InterfaceOld.Value, InterfaceOld.Value.left, InterfaceOld.Value.observe, InterfaceOld.Value.right, InterfaceOld.tensor, Packet, instNormBit, instNormForallFin_computerNetworks, instNormPacket

Mathlib dependencies: Finset, Norm

Lean core dependencies: And, Bool, Eq, Exists, Fin, List, List.length, Nat, Nonempty, Option, Unit, Unit.unit

Used by: (none)

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