Compiled Factorization Checks

The packed tensor runtime uses native externs, so executable examples run through a compiled lean_exe rather than the Lean interpreter.

def NN.Examples.Factorization.checkAll : IO Unit

Run the Cholesky and QR positive checks and their negative controls.

def NN.Examples.Factorization.usage : String

Command-line help for the compiled factorization checks.

def NN.Examples.Factorization.main (args : List String) : IO Unit

Entry point: run every factorization check, positive cases and negative controls alike.