kdrag.theories.option

Algebraic data type for optional values

Functions

`None_`(T)	Helper to create Option None_ values >>> None_(smt.IntSort()) None_
`get`(x, default)	Get the value of an Option, or a default value if it is None_ >>> get(kd.Some(42), 0) If(is(Some, Some(42)), val(Some(42)), 0)
`is_option`(x)	Check if a value is an Option >>> is_option(kd.Some(42)) True >>> is_option(42) False

kdrag.theories.option.None_(T: SortRef) → DatatypeRef

Helper to create Option None_ values >>> None_(smt.IntSort()) None_

kdrag.theories.option.get(x: DatatypeRef, default: ExprRef) → ExprRef

Get the value of an Option, or a default value if it is None_ >>> get(kd.Some(42), 0) If(is(Some, Some(42)), val(Some(42)), 0)

Parameters:

Return type:

ExprRef

kdrag.theories.option.is_option(x: DatatypeRef) → bool

Check if a value is an Option >>> is_option(kd.Some(42)) True >>> is_option(42) False