Charge one owned allocation, rounded independently of its neighbors. An
alias is not an allocation; target inventories omit it before this step.
56def nativeMemoryLease =
57 (lambda unrestricted identity : Bytes .
58 (lambda unrestricted endpoint : Nat .
59 (lambda unrestricted domain : Nat .
60 (lambda unrestricted quantum : Nat .
61 (lambda unrestricted extent : Nat .
62 (eliminate
63 StdResult
64 (lambda unrestricted current : (family StdResult (family NativePhysicalMemoryFailure) Nat) .
65 (family StdResult (family NativePhysicalMemoryFailure) (family ResourceLease)))
66 (nativeMemoryMappedBytes quantum extent)
67 (branch
68 StdFailure
69 error
70 .
71 (constructor
72 StdResult
73 StdFailure
74 (family NativePhysicalMemoryFailure)
75 (family ResourceLease)
76 error))
77 (branch
78 StdSuccess
79 bytes
80 .
81 (constructor
82 StdResult
83 StdSuccess
84 (family NativePhysicalMemoryFailure)
85 (family ResourceLease)
86 (constructor
87 ResourceLease
88 ResourceLeaseOf
89 identity
90 endpoint
91 domain
92 (constructor ResourceUnit ResourceMemoryBytes)
93 bytes
94 0
95 1)))))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.