~/bend-docscommunity

general/rose/LAWS.bend open laws/TODOs

raw source on the hub · import 0x635d6b0e0ec6a1b1f1319bf06aa496d9/general/rose/LAWS.bend as LAWS

3 imports
import Base
import ./type.bend as R
import ./ops.bend as O

Laws

law first_key_is_own provedin general/rose/PROOF.bendsource · line 6 · raw

@-N:Data -> @+r:0x635d6b0e0ec6a1b1f1319bf06aa496d9/general/rose/type.Rose<N> -> {0x635d6b0e0ec6a1b1f1319bf06aa496d9/general/rose/ops.first(0x635d6b0e0ec6a1b1f1319bf06aa496d9/general/rose/ops.keys(N, [r])) == 0x635d6b0e0ec6a1b1f1319bf06aa496d9/general/rose/ops.key(N, r) : String}

LAW: a tree's first key is its own