Reservoir

xubaiw/lean4-terminal

(WIP) Cross platform terminal package for Lean 4.

GitHub Link Documentation

Pick a version!

TODO: should show a time axes that allows the users to view, filter and click copy the lakefile config.

README

lean4-terminal

WIP: event feature not finished.

A Lean package for programming the terminal.

This pacakge is mostly "translated" from Rust's crossterm.

Example

import Terminal

open Terminal

def main : IO Unit := do
  queue #[
    Terminal.SetBackgroundColor.mk Color.red
  ]
  IO.println "Hello, world"

Limitations

  • stdout only, until IO primitives for Lean 4 is more usable.
  • ANSI only (Win 10 and *nix). Adding support for legacy systems is important, but not our focus now.
  • poll unavailable, lacking of async IO in Lean 4.