def h.wf_nil

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

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

2851def h.wf_nil(~K: Data, ~V: Data, ~hash: K -> U32, ~eq: K -> K -> Bool, n: Nat)
2852  -> {h.WF(~K, ~V, ~hash, ~eq, n, M.HNil{}) == True{} : Bool}:
2853  match n:
2854    case 0n:
2855      {==}
2856    case 1n+p:
2857      {==}