For internal spidr use only.
data Err : TypeOutOfBounds : Nat -> Nat -> ErrValueNotFound : Nat -> ErrPjrtErr : PjrtError -> ErrMlirPassError : String -> ErrInvalidHloError : String -> ErrShow Err0 ErrIO : Type -> Typedata TensorData : (Shape -> DType -> Type) -> Shape -> DType -> TypeMkTensorData : f shape dtype -> TensorData f shape dtypeexecute : Device -> Fn 0 -> All2 (TensorData (\{_:9570}, {_:9573} => ())) shapes dtypes -> ErrIO (All2 (TensorData (\{_:9582} => Array . idrisType)) shapes dtypes)