~/bend-docscommunity

general/rose/LAWS.bend open laws/TODOs

raw source on the hub · import 0xc4f31b1cf377fad1ed5191443ddd1c20/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:0xc4f31b1cf377fad1ed5191443ddd1c20/general/rose/type.Rose<N> -> {0xc4f31b1cf377fad1ed5191443ddd1c20/general/rose/ops.first(0xc4f31b1cf377fad1ed5191443ddd1c20/general/rose/ops.keys(N, [r])) == 0xc4f31b1cf377fad1ed5191443ddd1c20/general/rose/ops.key(N, r) : String}

LAW: a tree's first key is its own