hara.runtime.basic.impl-annex.process-lean

(sh-exec-lean input-args input-body {:keys [trim stderr raw root extension], :as opts, :or {trim clojure.string/trim-newline}})

Executes a Lean source file and returns its #eval output.

(sh-exec-lean-docker input-args input-body {:keys [trim stderr raw root extension container], :as opts, :or {trim clojure.string/trim-newline}})

Executes a Lean source file inside a Docker container.

(sh-exec-lean-portable input-args input-body {:keys [container container-backup force-container], :as opts})

Uses local Lean when available and otherwise falls back to Docker.

(transform-form forms opts)

Transforms forms into a standalone Lean script ending in #eval.

Generated by Codox