Expand description
BranchPath — opaque identifier for a branch in the structural tree of
!/?! groups. Used in Oracle-proof specs for generative effects
(oracle : (BranchPath, Int, args...) -> T) and, via the trace-API
.path() bridge, for tying trace events to oracle invocations.
Three constructors — the only way to obtain a BranchPath:
BranchPath.root : () -> BranchPath— canonical root.BranchPath.child : (BranchPath, Int) -> BranchPath— extend a path by entering a branch of a group.BranchPath.parse : String -> BranchPath— parse dewey-decimal ("2.0"), used to bridge recordings to specs.
Internal representation is a record { dewey: String } — user code
cannot construct arbitrary paths because the field is not exposed as a
public member and record-literal construction of built-in types isn’t
available at the surface.