Skip to content

Split Example

This example illustrates a transformation operator informally.

Operator

text SP split

Intuition

A split divides a referent into two or more constituent components, each of which may itself be a referent.

Formal authority

The authoritative operator definition is in:

text SE/Transformation/Domain/Operator/Codes.lean SE/Transformation/Domain/Operator/Labels.lean SE/Transformation/Domain/Operator/Semantics.lean

Rule

Split describes division.