Arrays over nullables, sort-erased

One lifted constructor per liftable operator, <id>?, each answering none unless every argument is some.

select? and store? take and answer nullable terms: it is the array term that becomes nullable, not its indices or elements. An array whose elements are themselves nullable is a different thing, of sort (Array I (Nullable E)).

def Cvc.Untyped.Term.eqRange? [Ω] (lft rgt lo hi : Term) : Env Term

eqRange lifted over nullables, strictly: none unless every argument is some.

Equations

• lft.eqRange? rgt lo hi = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.EQ_RANGE #[lft, rgt, lo, hi]

def Cvc.Untyped.Term.store? [Ω] (arr idx elm : Term) : Env Term

store lifted over nullables, strictly: none unless every argument is some.

Equations

• arr.store? idx elm = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.STORE #[arr, idx, elm]

def Cvc.Untyped.Term.select? [Ω] (arr idx : Term) : Env Term

select lifted over nullables, strictly: none unless every argument is some.

Equations

• arr.select? idx = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.SELECT #[arr, idx]