Documentation

Actus.Protocol

inductive Actus.Protocol.ContractType :

Instances For

@[implicit_reducible]

instance Actus.Protocol.instReprContractType :

Repr ContractType

Equations

Actus.Protocol.instReprContractType = { reprPrec := Actus.Protocol.instReprContractType.repr }

def Actus.Protocol.instReprContractType.repr :

ContractType → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Actus.Protocol.instDecidableEqContractType :

DecidableEq ContractType

Equations

Actus.Protocol.instDecidableEqContractType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Actus.Protocol.ContractRole :

CR_RPA : ContractRole
CR_RPL : ContractRole
CR_CLO : ContractRole
CR_CNO : ContractRole
CR_COL : ContractRole
CR_LG : ContractRole
CR_ST : ContractRole
CR_BUY : ContractRole
CR_SEL : ContractRole
CR_RFL : ContractRole
CR_PFL : ContractRole
CR_RF : ContractRole
CR_PF : ContractRole

Instances For

def Actus.Protocol.instReprContractRole.repr :

ContractRole → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Actus.Protocol.instReprContractRole :

Repr ContractRole

Equations

Actus.Protocol.instReprContractRole = { reprPrec := Actus.Protocol.instReprContractRole.repr }

@[implicit_reducible]

instance Actus.Protocol.instDecidableEqContractRole :

DecidableEq ContractRole

Equations

Actus.Protocol.instDecidableEqContractRole x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Actus.Protocol.DayCountConvention :

DCC_A_AISDA : DayCountConvention
DCC_A_360 : DayCountConvention
DCC_A_365 : DayCountConvention
DCC_E30_360ISDA : DayCountConvention
DCC_E30_360 : DayCountConvention
DCC_B_252 : DayCountConvention

Instances For

@[implicit_reducible]

instance Actus.Protocol.instReprDayCountConvention :

Repr DayCountConvention

Equations

Actus.Protocol.instReprDayCountConvention = { reprPrec := Actus.Protocol.instReprDayCountConvention.repr }

def Actus.Protocol.instReprDayCountConvention.repr :

DayCountConvention → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Actus.Protocol.instDecidableEqDayCountConvention :

DecidableEq DayCountConvention

Equations

Actus.Protocol.instDecidableEqDayCountConvention x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Actus.Protocol.EndOfMonthConvention :

EOMC_EOM : EndOfMonthConvention
EOMC_SD : EndOfMonthConvention

Instances For

def Actus.Protocol.instReprEndOfMonthConvention.repr :

EndOfMonthConvention → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Actus.Protocol.instReprEndOfMonthConvention :

Repr EndOfMonthConvention

Equations

Actus.Protocol.instReprEndOfMonthConvention = { reprPrec := Actus.Protocol.instReprEndOfMonthConvention.repr }

@[implicit_reducible]

instance Actus.Protocol.instDecidableEqEndOfMonthConvention :

DecidableEq EndOfMonthConvention

Equations

Actus.Protocol.instDecidableEqEndOfMonthConvention x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Actus.Protocol.BusinessDayConvention :

Instances For

@[implicit_reducible]

instance Actus.Protocol.instReprBusinessDayConvention :

Repr BusinessDayConvention

Equations

Actus.Protocol.instReprBusinessDayConvention = { reprPrec := Actus.Protocol.instReprBusinessDayConvention.repr }

def Actus.Protocol.instReprBusinessDayConvention.repr :

BusinessDayConvention → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Actus.Protocol.instDecidableEqBusinessDayConvention :

DecidableEq BusinessDayConvention

Equations

Actus.Protocol.instDecidableEqBusinessDayConvention x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Actus.Protocol.Calendar :

CLDR_MF : Calendar
CLDR_NC : Calendar

Instances For

@[implicit_reducible]

instance Actus.Protocol.instReprCalendar :

Equations

Actus.Protocol.instReprCalendar = { reprPrec := Actus.Protocol.instReprCalendar.repr }

def Actus.Protocol.instReprCalendar.repr :

Calendar → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Actus.Protocol.instDecidableEqCalendar :

DecidableEq Calendar

Equations

Actus.Protocol.instDecidableEqCalendar x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure Actus.Protocol.ScheduleConfig :

calendar : Option Calendar
endOfMonthConvention : Option EndOfMonthConvention
businessDayConvention : Option BusinessDayConvention

Instances For

def Actus.Protocol.instReprScheduleConfig.repr :

ScheduleConfig → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Actus.Protocol.instReprScheduleConfig :

Repr ScheduleConfig

Equations

Actus.Protocol.instReprScheduleConfig = { reprPrec := Actus.Protocol.instReprScheduleConfig.repr }

inductive Actus.Protocol.Performance :

PRF_PF : Performance
PRF_DL : Performance
PRF_DQ : Performance
PRF_DF : Performance

Instances For

@[implicit_reducible]

instance Actus.Protocol.instReprPerformance :

Repr Performance

Equations

Actus.Protocol.instReprPerformance = { reprPrec := Actus.Protocol.instReprPerformance.repr }

def Actus.Protocol.instReprPerformance.repr :

Performance → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Actus.Protocol.instDecidableEqPerformance :

DecidableEq Performance

Equations

Actus.Protocol.instDecidableEqPerformance x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Actus.Protocol.CreditEventTypeCovered :

Instances For

@[implicit_reducible]

instance Actus.Protocol.instReprCreditEventTypeCovered :

Repr CreditEventTypeCovered

Equations

Actus.Protocol.instReprCreditEventTypeCovered = { reprPrec := Actus.Protocol.instReprCreditEventTypeCovered.repr }

def Actus.Protocol.instReprCreditEventTypeCovered.repr :

CreditEventTypeCovered → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Actus.Protocol.instDecidableEqCreditEventTypeCovered :

DecidableEq CreditEventTypeCovered

Equations

Actus.Protocol.instDecidableEqCreditEventTypeCovered x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Actus.Protocol.CreditEventGuaranteedExposure :

CEGE_NO : CreditEventGuaranteedExposure
CEGE_NI : CreditEventGuaranteedExposure

Instances For

def Actus.Protocol.instReprCreditEventGuaranteedExposure.repr :

CreditEventGuaranteedExposure → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Actus.Protocol.instReprCreditEventGuaranteedExposure :

Repr CreditEventGuaranteedExposure

Equations

Actus.Protocol.instReprCreditEventGuaranteedExposure = { reprPrec := Actus.Protocol.instReprCreditEventGuaranteedExposure.repr }

@[implicit_reducible]

instance Actus.Protocol.instDecidableEqCreditEventGuaranteedExposure :

DecidableEq CreditEventGuaranteedExposure

Equations

Actus.Protocol.instDecidableEqCreditEventGuaranteedExposure x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Actus.Protocol.FeeBasis :

FEB_A : FeeBasis
FEB_N : FeeBasis

Instances For

def Actus.Protocol.instReprFeeBasis.repr :

FeeBasis → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Actus.Protocol.instReprFeeBasis :

Equations

Actus.Protocol.instReprFeeBasis = { reprPrec := Actus.Protocol.instReprFeeBasis.repr }

@[implicit_reducible]

instance Actus.Protocol.instDecidableEqFeeBasis :

DecidableEq FeeBasis

Equations

Actus.Protocol.instDecidableEqFeeBasis x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Actus.Protocol.InterestCalculationBase :

Instances For

@[implicit_reducible]

instance Actus.Protocol.instReprInterestCalculationBase :

Repr InterestCalculationBase

Equations

Actus.Protocol.instReprInterestCalculationBase = { reprPrec := Actus.Protocol.instReprInterestCalculationBase.repr }

def Actus.Protocol.instReprInterestCalculationBase.repr :

InterestCalculationBase → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Actus.Protocol.instDecidableEqInterestCalculationBase :

DecidableEq InterestCalculationBase

Equations

Actus.Protocol.instDecidableEqInterestCalculationBase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Actus.Protocol.ScalingEffect :

SE_OOO : ScalingEffect
SE_IOO : ScalingEffect
SE_ONO : ScalingEffect
SE_OOM : ScalingEffect
SE_INO : ScalingEffect

Instances For

def Actus.Protocol.instReprScalingEffect.repr :

ScalingEffect → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Actus.Protocol.instReprScalingEffect :

Repr ScalingEffect

Equations

Actus.Protocol.instReprScalingEffect = { reprPrec := Actus.Protocol.instReprScalingEffect.repr }

@[implicit_reducible]

instance Actus.Protocol.instDecidableEqScalingEffect :

DecidableEq ScalingEffect

Equations

Actus.Protocol.instDecidableEqScalingEffect x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Actus.Protocol.PenaltyType :

PYTP_A : PenaltyType
PYTP_N : PenaltyType
PYTP_I : PenaltyType
PYTP_O : PenaltyType

Instances For

def Actus.Protocol.instReprPenaltyType.repr :

PenaltyType → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Actus.Protocol.instReprPenaltyType :

Repr PenaltyType

Equations

Actus.Protocol.instReprPenaltyType = { reprPrec := Actus.Protocol.instReprPenaltyType.repr }

@[implicit_reducible]

instance Actus.Protocol.instDecidableEqPenaltyType :

DecidableEq PenaltyType

Equations

Actus.Protocol.instDecidableEqPenaltyType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Actus.Protocol.PrepaymentEffect :

Instances For

def Actus.Protocol.instReprPrepaymentEffect.repr :

PrepaymentEffect → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Actus.Protocol.instReprPrepaymentEffect :

Repr PrepaymentEffect

Equations

Actus.Protocol.instReprPrepaymentEffect = { reprPrec := Actus.Protocol.instReprPrepaymentEffect.repr }

@[implicit_reducible]

instance Actus.Protocol.instDecidableEqPrepaymentEffect :

DecidableEq PrepaymentEffect

Equations

Actus.Protocol.instDecidableEqPrepaymentEffect x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Actus.Protocol.DeliverySettlement :

DS_S : DeliverySettlement
DS_D : DeliverySettlement

Instances For

def Actus.Protocol.instReprDeliverySettlement.repr :

DeliverySettlement → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Actus.Protocol.instReprDeliverySettlement :

Repr DeliverySettlement

Equations

Actus.Protocol.instReprDeliverySettlement = { reprPrec := Actus.Protocol.instReprDeliverySettlement.repr }

@[implicit_reducible]

instance Actus.Protocol.instDecidableEqDeliverySettlement :

DecidableEq DeliverySettlement

Equations

Actus.Protocol.instDecidableEqDeliverySettlement x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Actus.Protocol.ObjectCodeCollateral :

OBJC_A : ObjectCodeCollateral
OBJC_N : ObjectCodeCollateral

Instances For

@[implicit_reducible]

instance Actus.Protocol.instReprObjectCodeCollateral :

Repr ObjectCodeCollateral

Equations

Actus.Protocol.instReprObjectCodeCollateral = { reprPrec := Actus.Protocol.instReprObjectCodeCollateral.repr }

def Actus.Protocol.instReprObjectCodeCollateral.repr :

ObjectCodeCollateral → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Actus.Protocol.instDecidableEqObjectCodeCollateral :

DecidableEq ObjectCodeCollateral

Equations

Actus.Protocol.instDecidableEqObjectCodeCollateral x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Actus.Protocol.Seniority :

SE_S : Seniority
SE_J : Seniority

Instances For

@[implicit_reducible]

instance Actus.Protocol.instReprSeniority :

Equations

Actus.Protocol.instReprSeniority = { reprPrec := Actus.Protocol.instReprSeniority.repr }

def Actus.Protocol.instReprSeniority.repr :

Seniority → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Actus.Protocol.instDecidableEqSeniority :

DecidableEq Seniority

Equations

Actus.Protocol.instDecidableEqSeniority x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure Actus.Protocol.Cycle :

n : Nat
period : String
stub : Bool

Instances For

def Actus.Protocol.instReprCycle.repr :

Cycle → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Actus.Protocol.instReprCycle :

Equations

Actus.Protocol.instReprCycle = { reprPrec := Actus.Protocol.instReprCycle.repr }

structure Actus.Protocol.Period :

n : Nat
period : String
isLongStub : Bool

Instances For

def Actus.Protocol.instReprPeriod.repr :

Period → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Actus.Protocol.instReprPeriod :

Equations

Actus.Protocol.instReprPeriod = { reprPrec := Actus.Protocol.instReprPeriod.repr }

inductive Actus.Protocol.ReferenceRole :

Instances For

def Actus.Protocol.instReprReferenceRole.repr :

ReferenceRole → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Actus.Protocol.instReprReferenceRole :

Repr ReferenceRole

Equations

Actus.Protocol.instReprReferenceRole = { reprPrec := Actus.Protocol.instReprReferenceRole.repr }

@[implicit_reducible]

instance Actus.Protocol.instDecidableEqReferenceRole :

DecidableEq ReferenceRole

Equations

Actus.Protocol.instDecidableEqReferenceRole x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure Actus.Protocol.LocalTime :

day : Nat
month : Nat
year : Nat

Instances For

def Actus.Protocol.instReprLocalTime.repr :

LocalTime → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Actus.Protocol.instReprLocalTime :

Equations

Actus.Protocol.instReprLocalTime = { reprPrec := Actus.Protocol.instReprLocalTime.repr }

inductive Actus.Protocol.Reference (α : Type) :

referenceTerms {α : Type} : ContractTerms α → Reference α
referenceId {α : Type} : String → Reference α

Instances For

inductive Actus.Protocol.ContractStructure (α : Type) :

mk {α : Type} : Reference α → ReferenceRole → ContractType → ContractStructure α

Instances For

structure Actus.Protocol.ContractTerms (α : Type) :

contractId : String
contractType : ContractType
contractRole : ContractRole
settlementCurrency : Option String
initialExchangeDate : Option LocalTime
dayCountConvention : Option DayCountConvention
scheduleConfig : ScheduleConfig
statusDate : LocalTime
marketObjectCodeRef : Option String
contractPerformance : Option Performance
creditEventTypeCovered : Option CreditEventTypeCovered
coverageOfCreditEnhancement : Option α
guaranteedExposure : Option CreditEventGuaranteedExposure
cycleOfFee : Option Cycle
cycleAnchorDateOfFee : Option LocalTime
feeAccrued : Option α
feeBasis : Option FeeBasis
feeRate : Option α
cycleAnchorDateOfInterestPayment : Option LocalTime
cycleOfInterestPayment : Option Cycle
accruedInterest : Option α
capitalizationEndDate : Option LocalTime
cycleAnchorDateOfInterestCalculationBase : Option LocalTime
cycleOfInterestCalculationBase : Option Cycle
interestCalculationBase : Option InterestCalculationBase
interestCalculationBaseA : Option α
nominalInterestRate : Option α
nominalInterestRate2 : Option α
interestScalingMultiplier : Option α
maturityDate : Option LocalTime
amortizationDate : Option LocalTime
exerciseDate : Option LocalTime
notionalPrincipal : Option α
notionalPrincipal2 : Option α
premiumDiscountAtIED : Option α
cycleAnchorDateOfPrincipalRedemption : Option LocalTime
cycleOfPrincipalRedemption : Option Cycle
nextPrincipalRedemptionPayment : Option α
arrayCycleAnchorDateOfInterestPayment : Option (List LocalTime)
arrayCycleOfInterestPayment : Option (List (Option Cycle))
arrayCycleAnchorDateOfPrincipalRedemption : Option (List LocalTime)
arrayCycleOfPrincipalRedemption : Option (List (Option Cycle))
arrayNextPrincipalRedemptionPayment : Option (List α)
arrayIncreaseDecrease : Option (List String)
arrayCycleAnchorDateOfRateReset : Option (List LocalTime)
arrayRate : Option (List α)
arrayFixedVariable : Option (List String)
purchaseDate : Option LocalTime
priceAtPurchaseDate : Option α
terminationDate : Option LocalTime
priceAtTerminationDate : Option α
quantity : Option α
currency : Option String
currency2 : Option String
scalingIndexAtStatusDate : Option α
cycleAnchorDateOfScalingIndex : Option LocalTime
cycleOfScalingIndex : Option Cycle
scalingEffect : Option ScalingEffect
scalingIndexAtContractDealDate : Option α
marketObjectCodeOfScalingIndex : Option String
notionalScalingMultiplier : Option α
cycleOfOptionality : Option Cycle
cycleAnchorDateOfOptionality : Option LocalTime
optionStrike1 : Option α
optionType : Option String
optionExerciseType : Option String
settlementPeriod : Option Cycle
exerciseAmount : Option α
futuresPrice : Option α
xDayNotice : Option Cycle
penaltyRate : Option α
penaltyType : Option PenaltyType
prepaymentEffect : Option PrepaymentEffect
cycleOfRateReset : Option Cycle
cycleAnchorDateOfRateReset : Option LocalTime
nextResetRate : Option α
rateSpread : Option α
rateMultiplier : Option α
periodFloor : Option α
periodCap : Option α
lifeCap : Option α
lifeFloor : Option α
marketObjectCodeOfRateReset : Option String
cycleOfDividend : Option Cycle
cycleAnchorDateOfDividend : Option LocalTime
nextDividendPaymentAmount : Option α
marketObjectCodeOfDividends : Option String
contractStructure : Option (List (ContractStructure α))
deliverySettlement : Option String
enableSettlement : Bool

Instances For

inductive Actus.Protocol.EventType :

AD : EventType
IED : EventType
FP : EventType
PR : EventType
PD : EventType
PRD : EventType
TD : EventType
IP : EventType
IPCI : EventType
IPCB : EventType
RR : EventType
RRF : EventType
DV : EventType
PRF : EventType
PY : EventType
PP : EventType
CD : EventType
STD : EventType
MD : EventType
XD : EventType
SC : EventType
CE : EventType
PI : EventType
IPFX : EventType
IPFL : EventType

Instances For

@[implicit_reducible]

instance Actus.Protocol.instReprEventType :

Equations

Actus.Protocol.instReprEventType = { reprPrec := Actus.Protocol.instReprEventType.repr }

def Actus.Protocol.instReprEventType.repr :

EventType → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Actus.Protocol.instDecidableEqEventType :

DecidableEq EventType

Equations

Actus.Protocol.instDecidableEqEventType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Actus.Protocol.eventTypePriority :

EventType → Nat

Priority for intra-timestamp event ordering (lower = processed first). Order derived from the ACTUS reference event sequences: in particular PR < IP, IP before rate resets / scaling / IPCB, and interest (IP) before contract-closing events (PRD, TD, MD) so it accrues on the full notional before the contract is purchased/terminated/matured.

Equations

Instances For

def Actus.Protocol.eventTypeToString :

EventType → String

String representation of an event type.

Equations

Instances For

inductive Actus.Protocol.RiskFactor :

CURS : Float → RiskFactor
XXXX : Float → RiskFactor

Instances For

@[implicit_reducible]

instance Actus.Protocol.instReprRiskFactor :

Repr RiskFactor

Equations

Actus.Protocol.instReprRiskFactor = { reprPrec := Actus.Protocol.instReprRiskFactor.repr }

def Actus.Protocol.instReprRiskFactor.repr :

RiskFactor → Nat → Std.Format

Equations

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

Instances For

@[reducible, inline]

abbrev Actus.Protocol.Time :

Equations

Actus.Protocol.Time = Nat

Instances For

@[reducible, inline]

abbrev Actus.Protocol.Payoff :

Equations

Actus.Protocol.Payoff = Float

Instances For

@[reducible, inline]

abbrev Actus.Protocol.Event :

Equations

Actus.Protocol.Event = (Actus.Protocol.Time × Actus.Protocol.EventType)

Instances For

@[reducible, inline]

abbrev Actus.Protocol.Cashflow :

Equations

Actus.Protocol.Cashflow = (Actus.Protocol.Event × Actus.Protocol.Payoff)

Instances For

@[reducible, inline]

abbrev Actus.Protocol.Schedule :

Equations

Actus.Protocol.Schedule = List Actus.Protocol.Event

Instances For

@[reducible, inline]

abbrev Actus.Protocol.Cashflows :

Equations

Actus.Protocol.Cashflows = List Actus.Protocol.Cashflow

Instances For