Lean4-Socket

A toy implementation of socket programming for Lean 4.

Installation

Lake

import Lake
open System Lake DSL

package foo where
  dependencies := #[{
    name := `socket
    src := Source.git "https://github.com/xubaiw/lean4-socket.git" "main"
  }]

Usage

This prints out yout local address.

import Socket
open Socket

def main : IO Unit := do
  let addr ← SockAddr.mk "localhost" "8080"
  IO.println addr

Documentation

The documentation generated by doc-gen4 can be found here.

There are also basic usage in the examples directory.

Limitations

• Many low level flags are unavailable now.
• Only blocking sockets are supported.
• No dependent type and linear constraints.