inductive
definition
def or abbrev
MonetaryTool
show as:
view Lean formalization →
formal statement (Lean)
16inductive MonetaryTool where
17 | openMarket
18 | discountRate
19 | reserveRequirement
20 | qe
21 | forwardGuidance
22 deriving DecidableEq, Repr, BEq, Fintype
23