Encodings for bounded and optional control labels

@[instance_reducible]

instance MIPRE.Cost.instSizedEncodingFin {n : ℕ} : SizedEncoding (Fin n)

Finite numeric labels retain the ambient binary natural encoding.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance MIPRE.Cost.instSizedEncodingOption {α : Type u_1} [SizedEncoding α] : SizedEncoding (Option α)

An empty tree represents absence; a tagged pair represents presence.

Equations

• One or more equations did not get rendered due to their size.