def h.wf_leaf_o

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

import Base
import bend-mathlib@0.7.4.0/bool.bend as MBool
import bend-kit-collections@0.1.4.1/LAWS.bend as Laws
import bend-kit-collections@0.1.4.1/hmap.bend as M

3710def h.wf_leaf_o(
3711  ~K: Data, ~V: Data, ~hash: K -> U32, ~eq: K -> K -> Bool, p: Nat, +o: U32,
3712  +es: List<&2, M.Entry<K, V>>,
3713  hs: {Laws.hmap_hashed(~K, ~V, ~hash, es, o) == True{} : Bool},
3714  ds: {Laws.hmap_distinct(~K, ~V, ~eq, es) == True{} : Bool}
3715) -> {h.WF(~K, ~V, ~hash, ~eq, p, M.HLeaf{o, es}) == True{} : Bool}:
3716  match p:
3717    case 0n:
3718      ds
3719    case 1n+q:
3720      MBool.and_eq_true(Laws.hmap_hashed(~K, ~V, ~hash, es, o), Laws.hmap_distinct(~K, ~V, ~eq, es), hs, ds)