Lean4 Kernel - Interactive UI
Environments
No environment selected
New Environment
Refresh
Click "Refresh" to load
Expression Templates
Types
Prop
Type
Type u
Nat
Bool
Const
Expressions
BVar
App
Lambda
Forall
Let
Lit Nat
Levels
Zero
Succ
Param
Max
Names
Anonymous
String
Numeric
Quick Actions
List Constants
List Modules
Add Quot
Axiom
Definition
Theorem
Inductive
Constants
Add Axiom
Name
Level Parameters (comma-separated)
Leave empty for no universe parameters
Type (JSON expression)
Unsafe
Add Axiom
Preview JSON
Add Definition
Name
Level Parameters (comma-separated)
Type (JSON expression)
Value (JSON expression)
Hints
Opaque
Abbreviation
Regular
Safety
Safe
Unsafe
Partial
Add Definition
Preview JSON
Add Theorem
Name
Level Parameters (comma-separated)
Type (JSON expression) - the proposition
Value (JSON expression) - the proof
Add Theorem
Preview JSON
Add Inductive Type
Name
Level Parameters (comma-separated)
Number of Parameters
Type (JSON expression)
Constructors (JSON array)
Unsafe
Add Inductive
Preview JSON
Get Constant
Constant Name
Get Info
Typecheck
Modules
Module Name
Mark Loaded
Request
Ready
Response
Copy Response
Clear
GoLean4Kernel
|
Copyright 2026 S||nS
Docs
API