~/jendhub

def replace_read_owner

stelliferous@0.0.2.0 · proofs/storage_refinement.bend:420

import stelliferous@0.0.2.0/proofs/storage_refinement.bend as StorageRefinement
import Base

420# Used only in propositions to compare reads from different physical owners.
421def replace_read_owner(~Owner: Type,~Element: Data,owner: Owner,result: Owner & Element) -> Owner & Element:
422  (previous,value) = result
423  (owner,value)

Uses (2)

Used by (1)