This file defines Cedar decimal values and functions.

@[reducible, inline]

abbrev Cedar.Spec.Ext.DECIMAL_DIGITS : Nat

A decimal number consists of an integer part and a fractional part. The former is the integer number before the decimal point. The latter is the decimal number minus its integer part. For instance, 10.234 is a decimal number. Its integer part is 10 and its fractional part is 0.234 We restrict the number of the digits after the decimal point to 4.

Equations

• Cedar.Spec.Ext.DECIMAL_DIGITS = 4

@[reducible, inline]

abbrev Cedar.Spec.Ext.Decimal : Type

Equations

• Cedar.Spec.Ext.Decimal = Int64

def Cedar.Spec.Ext.Decimal.decimal? (i : Int) : Option Decimal

Create a Decimal from an Int representing its internal encoding. Most callers should use higher-level constructors, e.g., Decimal.parse

Equations

• Cedar.Spec.Ext.Decimal.decimal? i = Int64.ofInt? i

def Cedar.Spec.Ext.Decimal.parse (str : String) : Option Decimal

Equations

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

@[instance_reducible]

instance Cedar.Spec.Ext.Decimal.instToString : ToString Decimal

Equations

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

@[reducible, inline]

abbrev Cedar.Spec.Ext.Decimal.decimal (str : String) : Option Decimal

Equations

• Cedar.Spec.Ext.Decimal.decimal = Cedar.Spec.Ext.Decimal.parse