lean4-protobuf

A WIP Protobuf package for Lean 4.

Roadmap

• Parsing of .proto files (except for MessageValue constants, adding this is a TODO).
• Varint encoding and decoding.
• Type definition codegen. (Planning to support both an import_protobuf macro for doing this at compile time, as well as a protoc plugin for if you want to view and commit the generated code.)
• Encoding and decoding codegen. (Planning to do this with deriving ProtobufMessage.)
• Passing Protobuf conformance tests.
• Visibility refactor (ensure things that should be private are).
• Good docs and examples.