structure Lean.Compiler.LCNF.Simp.Config : Type

• If etaPoly is true, we eta expand any global function application when the function takes local instances. The idea is that we do not generate code for this kind of application, and we want all of them to specialized or inlined.

  etaPoly : Bool

• If inlinePartial is true, we inline partial function applications tagged with [inline]. Note that this option is automatically disabled when processing declarations tagged with [inline], marked to be specialized, or instances.

  inlinePartial : Bool

• If implementedBy is true, we apply the implemented_by replacements. Remark: we only apply casesOn replacements at phase 2 because cases constructor may not have enough information for reconstructing the original casesOn application at phase 1.

  implementedBy : Bool

• If inlineDefs is true then top-level definitions are inlined when they are small are annotated with inlining attributes.

  inlineDefs : Bool

Configuration options for Simp that are not controlled using set_option. Recall that we have multiple Simp passes and they use different configurations.

instance Lean.Compiler.LCNF.Simp.instInhabitedConfig : Inhabited Lean.Compiler.LCNF.Simp.Config

Equations

• Lean.Compiler.LCNF.Simp.instInhabitedConfig = { default := { etaPoly := default, inlinePartial := default, implementedBy := default, inlineDefs := default } }