~/bend-docscommunity

general/rose/LAWS.bend open laws/TODOs

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

LAW: a tree's first key is its own