def h.wf_leaf

bend-kit-collections@0.1.4.1 · PROOF.bend:2859

import Base
import bend-kit-collections@0.1.4.1/hmap.bend as M

2859def h.wf_leaf(
2860  ~K: Data, ~V: Data, ~hash: K -> U32, ~eq: K -> K -> Bool, +n: Nat, +o: U32,
2861  xs: List<&2, M.Entry<K, V>>, w: {h.WF(~K, ~V, ~hash, ~eq, n, M.HLeaf{o, xs}) == True{} : Bool}
2862) -> {h.WF(~K, ~V, ~hash, ~eq, n, M.HMap.leaf(K, V, o, xs)) == True{} : Bool}:
2863  match xs:
2864    case Nil{}:
2865      h.wf_nil(~K, ~V, ~hash, ~eq, n)
2866    case Con{e, rest}:
2867      w