Stdio.lean🔗

Standard I/O and Process Exit Syscalls

Re-exports Fs/ReadWrite.lean, Fs/ReadWritev.lean, and Kernel/Exit.lean, and defines the syscall dispatch tables and bundles Syscall.stdioWrite and Syscall.stdioCli.

@[expose] public section

namespace Arm64

namespace Syscall

1 declaration not shown (lines 31–33): theorems, which Lean checks, or definitions that no headline statement uses

Arm64.Syscall.stdioWriteTable

def stdioTableL35–55 ↗#

Dispatch table for standard stream I/O and process termination (read, write, readv, writev, exit, exit_group).

def stdioTable : List (BitVec 64 × (State → State)) :=
  [(SYS_READ, execRead),
   (SYS_WRITE, execWrite),
   (SYS_READV, execReadv),
   (SYS_WRITEV, execWritev),
   (SYS_EXIT, execExit),
   (SYS_EXIT_GROUP, execExit)]

2 declarations not shown (lines 45–50): theorems, which Lean checks, or definitions that no headline statement uses

Arm64.Syscall.stdioWrite, Arm64.Syscall.stdioCli

end Syscall

end Arm64