def Actus.Util.Schedule.toTime (d : Protocol.LocalTime) : Protocol.Time

Map a calendar date onto the Time axis (serial day number ≥ 0).

Equations

• Actus.Util.Schedule.toTime d = (Actus.Util.Date.toEpochDay d).toNat

def Actus.Util.Schedule.schedule (cfg : Protocol.ScheduleConfig) (s : Protocol.LocalTime) (c : Option Protocol.Cycle) (t : Protocol.LocalTime) (includeEnd : Bool := true) : List Protocol.LocalTime

Schedule function S(s, c, T, B) (§3.1).

• c = none yields the two-point schedule [s, T].
• otherwise the cyclic times up to T are generated; when includeEnd (the boolean B) T is appended, applying long/short stub correction to the final period. Each time has the contract's EOM and BDC conventions applied.

Equations

• One or more equations did not get rendered due to their size.
• Actus.Util.Schedule.schedule cfg s none t includeEnd = if includeEnd = true then [s, t] else [s]

def Actus.Util.Schedule.arraySchedule (cfg : Protocol.ScheduleConfig) (anchors : List (Protocol.LocalTime × Option Protocol.Cycle)) (tEnd : Protocol.LocalTime) : List Protocol.LocalTime

Array schedule S̄(s⃗, c⃗) (§3.2): concatenate S(sᵢ, cᵢ, sᵢ₊₁) over the successive anchor/cycle pairs, ending at tEnd.

Equations

• Actus.Util.Schedule.arraySchedule cfg anchors tEnd = Actus.Util.Schedule.arraySchedule.go cfg tEnd anchors

def Actus.Util.Schedule.arraySchedule.go (cfg : Protocol.ScheduleConfig) (tEnd : Protocol.LocalTime) : List (Protocol.LocalTime × Option Protocol.Cycle) → List Protocol.LocalTime

Equations

• Actus.Util.Schedule.arraySchedule.go cfg tEnd [] = []
• Actus.Util.Schedule.arraySchedule.go cfg tEnd [(s, c)] = Actus.Util.Schedule.schedule cfg s c tEnd
• Actus.Util.Schedule.arraySchedule.go cfg tEnd ((s, c) :: (s', c') :: rest) = Actus.Util.Schedule.schedule cfg s c s' false ++ Actus.Util.Schedule.arraySchedule.go cfg tEnd ((s', c') :: rest)

def Actus.Util.Schedule.annuity {α : Type} [Amount α] (n a r : α) (yfs : List α) : α

Annuity amount A(s,T,n,a,r) (§3.8): the constant total instalment that amortizes n + a over the payment periods whose year fractions are yfs (Y(tᵢ, tᵢ₊₁)), at rate r. Computed as the present-value annuity

A = (n + a) / Σₖ ∏_{j ≤ k} (1 + r·yfⱼ)⁻¹,

i.e. n + a divided by the sum of discount factors — the formulation the ACTUS reference uses. (Σₖ runs over the periods; the inner product is the discount factor to the end of period k.)

Equations

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