def EvmYul.Operation.pretty (self : Operation OperationType.EVM) : String

Strip the existing repr a'la:

• EvmYul.Operation.Push (EvmYul.Operation.POp.PUSH1) → PUSH1

This breaks the moment that Repr changes its behaviour; it is fine for the time being.

Equations

• self.pretty = ((toString (repr self)).splitOn ".").getLast!.take ((toString (repr self)).splitOn ".").getLast!.length.pred

def EvmYul.Finmap.pretty {α β : Type} [ToString α] [ToString β] [LE ((_ : α) × β)] [IsTrans ((_ : α) × β) fun (x x_1 : (_ : α) × β) => x ≤ x_1] [IsAntisymm ((_ : α) × β) fun (x x_1 : (_ : α) × β) => x ≤ x_1] [IsTotal ((_ : α) × β) fun (x x_1 : (_ : α) × β) => x ≤ x_1] [DecidableRel fun (x x_1 : (_ : α) × β) => x ≤ x_1] (self : Finmap fun (x : α) => β) : String

Finmaps are not very computation-friendly and so the API is ever so slightly meh; do feel encouraged to sorry out the order properties and just point it to an instance of LE.

TODO(not critical) - Unify all the maps used throught the formalisation one day.

Equations

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