Skip to content

Add UInt* byte seq instances #36

@JamesGallicchio

Description

@JamesGallicchio

See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Marshalling.20lean.20UInt*.20into.20byte.20arrays

I think the most sensible design is to add UInt*.BytesBE and UInt*.BytesLE wrapper structures, with UInt*.toBytes[BL]E functions. Then we can add Indexed instances on the wrapper structures, using Fin 2/4/8 as the index.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions