~/jendhub

def TraceState.from_entries.checked

bend-trace-context@0.2.0.0 · trace_context.bend:2343

import bend-trace-context@0.2.0.0/trace_context.bend as TraceContext
import Base

2343# The state of these entries when the check finds them valid, `fallback`
2344# otherwise. Updates build their entries so that the check passes, which the
2345# laws prove; `fallback` keeps the function total without an unchecked
2346# conversion.
2347def TraceState.from_entries.checked(entries: List<&2, StateEntry>, fallback: TraceState, valid: Bool,
2348  evidence: {TraceState.is_valid(entries) == valid : Bool}) -> TraceState:
2349  match valid:
2350    case True{}:
2351      TraceState{entries, evidence}
2352    case False{}:
2353      fallback

Uses (5)

Used by (1)