def Actus.Contract.CLM.stf {α : Type} [Amount α] (ct : Terms α) (rf : RiskFactorEnv α) (ev : Protocol.EventType) (t : Protocol.Time) (s : State α) : State α

CLM state transition = PAM's (the call-money specifics are in the schedule).

Equations

• Actus.Contract.CLM.stf ct rf ev t s = Actus.Contract.PAM.stf ct rf ev t s

def Actus.Contract.CLM.pof {α : Type} [Amount α] (ct : Terms α) (rf : RiskFactorEnv α) (ev : Protocol.EventType) (t : Protocol.Time) (s : State α) : α

CLM payoff = PAM's.

Equations

• Actus.Contract.CLM.pof ct rf ev t s = Actus.Contract.PAM.pof ct rf ev t s

def Actus.Contract.CLM.init {α : Type} [Amount α] (ct : Terms α) (md t₀ : Protocol.Time) : State α

CLM initial state = PAM's.

Equations

• Actus.Contract.CLM.init ct md t₀ = Actus.Contract.PAM.init ct md t₀

inductive Actus.Contract.CLM.Step {α : Type} [Amount α] (ct : Terms α) (rf : RiskFactorEnv α) : State α → State α → Type

• ev {α : Type} [Amount α] {ct : Terms α} {rf : RiskFactorEnv α} {s : State α} (e : Protocol.EventType) {t : Protocol.Time} : s.sd ≤ t → Step ct rf s (stf ct rf e t s)

@[reducible, inline]

abbrev Actus.Contract.CLM.Trace {α : Type} [Amount α] (ct : Terms α) (rf : RiskFactorEnv α) : State α → State α → Type

Equations

• Actus.Contract.CLM.Trace ct rf = Actus.Closures.Star (Actus.Contract.CLM.Step ct rf)

def Actus.Contract.CLM.getCashflow {α : Type} [Amount α] (ct : Terms α) (rf : RiskFactorEnv α) {s s' : State α} (h : Step ct rf s s') : Protocol.Event × α

Equations

• Actus.Contract.CLM.getCashflow ct rf (Actus.Contract.CLM.Step.ev e a) = (((Actus.Contract.CLM.stf ct rf e t s).sd, e), Actus.Contract.CLM.pof ct rf e (Actus.Contract.CLM.stf ct rf e t s).sd s)

def Actus.Contract.CLM.getCashflows {α : Type} [Amount α] (ct : Terms α) (rf : RiskFactorEnv α) {s s' : State α} : Trace ct rf s s' → List (Protocol.Event × α)

Equations

• Actus.Contract.CLM.getCashflows ct rf Actus.Closures.Star.refl = []
• Actus.Contract.CLM.getCashflows ct rf (Actus.Closures.Star.step h rest) = Actus.Contract.CLM.getCashflow ct rf h :: Actus.Contract.CLM.getCashflows ct rf rest

def Actus.Contract.CLM.CLM_contract : Abstract.ActusContract

Equations

• Actus.Contract.CLM.CLM_contract = { Terms := Actus.Contract.Terms Float, State := Actus.Contract.State Float }

def Actus.Contract.CLM.CLM_impl (ct : Terms Float) (rf : RiskFactorEnv Float) (s₀ : State Float) : Abstract.StateTransition CLM_contract

Equations

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