Theory Prefix_Match_toString

theory Prefix_Match_toString
imports IP_Address_toString Prefix_Match
begin

definition prefix_match_32_toString :: "32 prefix_match ⇒ string" where
  "prefix_match_32_toString pfx = (case pfx of PrefixMatch p l ⇒ ipv4addr_toString p @ (if l ≠ 32 then ''/'' @ string_of_nat l else []))"
definition prefix_match_128_toString :: "128 prefix_match ⇒ string" where
  "prefix_match_128_toString pfx = (case pfx of PrefixMatch p l ⇒ ipv6addr_toString p @ (if l ≠ 128 then ''/'' @ string_of_nat l else []))"

end