def default_after_presence
stelliferous@0.0.2.0 · proofs/storage_refinement.bend:315
import stelliferous@0.0.2.0/proofs/storage_refinement.bend as StorageRefinement
import Base
315def default_after_presence(~Element: Data,+fallback: Element,+present: Bool,+value: Element) ->
316 {Bool.pick(Element,present && True{},value,fallback) ==
317 Maybe.default(&2,Element,Bool.pick(Maybe<&2,Element>,present,Some{value},None{}),fallback) : Element}:
318 match present:
319 case False{}: {==}
320 case True{}: {==}