lean-py
Getting Started
Getting Started
Prerequisites
Installation
Quick Start
Pattern Matching (Python 3.10+)
Calling Python from Lean
Kernel Facade
Exception Handling
Next Steps
Setting Up a Project
Directory Layout
Step 1: Create the Lean Project
Step 2: Write Lean Code
Step 3: Build
Step 4: Create the Python Project
Step 5: Call Lean from Python
Using Additional Lake Dependencies
Type Marshalling Reference
Pattern Matching on Inductives
Examples
Basic Example
The Lean side
Exporting a function
Exporting a structure
Exporting an inductive
Making it all visible
The Python side
Running it
What to take away
Pantograph Kernel
Setting up
Loading an environment
Introspecting declarations
Running the elaborator
Creating goals and running tactics
Frontend processing
Goal state lifecycle
What to take away
Typed NumPy
The idea
Calling into Python
Reshape with proof obligations
A demo pipeline
Running it
What to take away
SymPy Tactic
The architecture
The oracle axiom
The Lean tactic
Converting Expr to SymPy
Using the tactic
Running
What to take away
Z3 / Knuckledragger Tactic
Same architecture, different solver
Converting Expr to Z3
Checking with Knuckledragger
Using the tactic
Running
Comparing SymPy and Z3
What to take away
Effectful Refinement-Type Verifier
The idea
The Lean side
Refinement annotations
Symbolic execution with effectful
Building Lean.Expr trees
De Bruijn indices
Converting Terms to Exprs with handlers
Verification via omega
The demo
What to take away
API Reference
Library Loading
Loading from a Lake project
Loading from a path
What happens at load time
Calling functions
Working with types
API reference
Kernel
Setup
Loading an environment
Querying declarations
Elaboration
Creating goals and running tactics
Prograde tactics
Conv and calc modes
Goal state lifecycle
Environment serialisation
Frontend processing
API reference
Kernel
GoalState
TacticResult
Marshalling
How values cross the boundary
Scalar types
Container types
Inductive types
LeanObj — owned pointers
LeanInductiveValue — Python-side inductives
Smart constructors
The Marshaller class
API reference
Registry
Where the data comes from
TypeRepr — describing Lean types
CtorInfo — constructor metadata
TypeInfo — type metadata
FuncInfo — function metadata
LibraryRegistry — the full picture
API reference
Exceptions
LeanError
LeanPyCallbackError
API reference
lean-py
Index
Index
C
|
D
|
F
|
G
|
K
|
M
|
P
|
R
|
S
|
T
C
collect_sorrys() (lean_py.kernel.Kernel method)
D
decide() (lean_py.kernel.Kernel method)
diag() (lean_py.kernel.GoalState method)
F
find_source_path() (lean_py.kernel.Kernel method)
G
goal_create() (lean_py.kernel.Kernel method)
goal_unpickle() (lean_py.kernel.Kernel method)
GoalState (class in lean_py.kernel)
K
Kernel (class in lean_py.kernel)
M
messages (lean_py.kernel.TacticResult attribute)
P
parse() (lean_py.kernel.TacticResult class method)
pickle() (lean_py.kernel.GoalState method)
process() (lean_py.kernel.Kernel method)
R
replay() (lean_py.kernel.GoalState method)
S
state (lean_py.kernel.TacticResult attribute)
status (lean_py.kernel.TacticResult attribute)
subsume() (lean_py.kernel.GoalState method)
T
TacticResult (class in lean_py.kernel)
try_define() (lean_py.kernel.GoalState method)
try_draft() (lean_py.kernel.GoalState method)
try_have() (lean_py.kernel.GoalState method)
try_let() (lean_py.kernel.GoalState method)