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

• etaPoly : Bool

  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.

• inlinePartial : 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.

• implementedBy : 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.

• inlineDefs : Bool

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

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 } }