Arrays over nullables, typed

Each lifted operator has its plain counterpart's signature with an Option around every argument and around the result, and nothing else changed. The lift is strict: 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, written TotalMap α (Option β).

def Cvc.Typed.Term.eqRange? [Ω] {ι κ : Type} [Ord ι] (lft rgt : Term (Option (TotalMap ι κ))) (lo hi : Term (Option ι)) : Env (Term (Option Bool))

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

Equations

• lft.eqRange? rgt lo hi = Cvc.Untyped.Term.eqRange? lft rgt lo hi

def Cvc.Typed.Term.store? [Ω] {ι κ : Type} [Ord ι] (arr : Term (Option (TotalMap ι κ))) (idx : Term (Option ι)) (elm : Term (Option κ)) : Env (Term (Option (TotalMap ι κ)))

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

Equations

• arr.store? idx elm = Cvc.Untyped.Term.store? arr idx elm

def Cvc.Typed.Term.select? [Ω] {ι κ : Type} [Ord ι] (arr : Term (Option (TotalMap ι κ))) (idx : Term (Option ι)) : Env (Term (Option κ))

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

Equations

• arr.select? idx = Cvc.Untyped.Term.select? arr idx