def Sparkle.Core.StateMacro.signalStateField : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Sparkle.Core.StateMacro.commandDeclare_signal_state__ : Lean.ParserDescr

declare_signal_state generates a synthesis-compatible state type alias, accessor defs, default value, and Inhabited instance from a field list.

Example:

declare_signal_state BottleneckState
  | fsmReg      : BitVec 2   := 0#2
  | residualReg : BitVec 8   := 0#8
  | resultReg   : BitVec 8   := 0#8
  | doneReg     : Bool       := false

Generates:

• abbrev BottleneckState := BitVec 2 × BitVec 8 × BitVec 8 × Bool
• BottleneckState.fsmReg, .residualReg, etc. accessor defs using projN!
• BottleneckState.default : BottleneckState
• instance : Inhabited BottleneckState

Equations

• One or more equations did not get rendered due to their size.