def pick_same

stelliferous@0.0.2.0 · proofs/storage_readback.bend:150

import Base

150# Every address of a fresh tree reads its fill value.
151def pick_same(~Element: Data,selected: Bool,+first: Element,+second: Element,+value: Element,first_equal: {first == value : Element},second_equal: {second == value : Element}) ->
152  {Bool.pick(Element,selected,first,second) == value : Element}:
153  match selected:
154    case True{}: first_equal
155    case False{}: second_equal