def h.gnil

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

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

2775def h.gnil(~K: Data, ~V: Data, ~eq: K -> K -> Bool, n: Nat, +mask: U32, +hk: U32, +k: K)
2776  -> {h.G(~K, ~V, ~eq, n, mask, M.HNil{}, hk, k) == None{} : Maybe<&2, V>}:
2777  match n:
2778    case 0n:
2779      {==}
2780    case 1n+p:
2781      {==}