def ba.hit

bend-osdev-algo@0.1.0.0 · PROOF.bend:1388

import Base
import bend-osdev-algo@0.1.0.0/bsearch.bend as S
import bend-osdev-algo@0.1.0.0/LAWS.bend as Laws

1388def ba.hit(b: Bool, +r: U32, +lb: Nat, +er: {U32.to_nat(r) == lb : Nat}) -> {Laws.algo_index_nat(Bool.pick(Maybe<&2, U32>, b, Some{r}, None{})) == S.bsearch.find.hit(b, lb) : Maybe<&2, Nat>}:
1389  match b:
1390    case True{}:
1391      Equal.cong(Nat, Maybe<&2, Nat>, z => Some{z}, U32.to_nat(r), lb, er)
1392    case False{}:
1393      {==}