Documentation

Lean.Compiler.Options

← Copula mathematical handbook
source
opaque Lean.Compiler.compiler.check :
Lean.Option Bool
source
opaque Lean.Compiler.compiler.traceUnnormalized :
Lean.Option Bool
source
opaque Lean.Compiler.compiler.checkMeta :
Lean.Option Bool
source
opaque Lean.Compiler.compiler.relaxedMetaCheck :
Lean.Option Bool
source
opaque Lean.Compiler.compiler.ignoreBorrowAnnotation :
Lean.Option Bool
source
opaque Lean.Compiler.compiler.postponeCompile :
Lean.Option Bool
source
opaque Lean.Compiler.compiler.inLeanIR :
Lean.Option Bool