opaque Sparkle.Compiler.hardwareModuleAttr : Lean.TagAttribute

@[hardware_module] — emit a Verilog sub-module for this definition instead of inlining its body.

opaque Sparkle.Compiler.inlineHardwareAttr : Lean.TagAttribute

@[inline_hardware] — historical alias for "always inline". Kept for backwards compatibility with code authored when the default was the opposite. Today the default is already inline, so this attribute documents intent without changing behaviour.

def Sparkle.Compiler.isHardwareModule (env : Lean.Environment) (name : Lean.Name) : Bool

True iff name is tagged @[hardware_module].

Equations

• Sparkle.Compiler.isHardwareModule env name = Sparkle.Compiler.hardwareModuleAttr.hasTag env name

def Sparkle.Compiler.isInlineHardware (env : Lean.Environment) (name : Lean.Name) : Bool

True iff name is tagged @[inline_hardware].

Equations

• Sparkle.Compiler.isInlineHardware env name = Sparkle.Compiler.inlineHardwareAttr.hasTag env name