Skip to main content

Module types

oxilean_codegen::lean4_backend

Module types 

Source
Expand description

Auto-generated module

🤖 Generated with SplitRS

Structs§

L4AnalysisCache
L4CacheEntry
L4ConstantFoldingHelper
L4DepGraph
L4DominatorTree
L4ExtCache
Analysis cache for L4Ext.
L4ExtConstFolder
Constant folding helper for L4Ext.
L4ExtDepGraph
Dependency graph for L4Ext.
L4ExtDomTree
Dominator tree for L4Ext.
L4ExtLiveness
Liveness analysis for L4Ext.
L4ExtPassConfig
Configuration for L4Ext passes.
L4ExtPassRegistry
Pass registry for L4Ext.
L4ExtPassStats
Statistics for L4Ext passes.
L4ExtWorklist
Worklist for L4Ext.
L4LivenessInfo
L4PassConfig
L4PassRegistry
L4PassStats
L4Worklist
Lean4Abbrev
A Lean 4 abbrev declaration (transparent definition).
Lean4Axiom
A Lean 4 axiom declaration.
Lean4Backend
Lean 4 code generation backend.
Lean4CalcStep
One step in a calc proof.
Lean4Constructor
A constructor of an inductive type.
Lean4Def
A Lean 4 def definition.
Lean4File
A complete Lean 4 source file.
Lean4Inductive
A Lean 4 inductive type declaration.
Lean4Instance
A Lean 4 instance declaration.
Lean4Structure
A Lean 4 structure declaration.
Lean4Theorem
A Lean 4 theorem declaration.

Enums§

L4ExtPassPhase
Pass execution phase for L4Ext.
L4PassPhase
Lean4Decl
Top-level Lean 4 declaration.
Lean4DoStmt
Statements in a do block.
Lean4Expr
Lean 4 expression representation.
Lean4Pattern
Pattern in a match expression.
Lean4Type
Lean 4 type representation.