Ghc.List
, Data.List
: size-related properties and termination
Data.Splay
: well-ordered trees and termination
Data.Map
: binary-search ordered trees and termination
Vector-Algorithms
: correctness of accessing, indexing and
slicing
Bytestring
: size-based low-level memory safety and termination
Text
: size-based pointer-safety and termination
184: measure fplen :: ForeignPtr a -> Int 185: 186: data ByteString = PS 187: { pay :: ForeignPtr Word8 188: , off :: {v:Nat | v <= (fplen pay)} 189: , len :: {v:Nat | off + v <= (fplen pay)} }
Allow us to enforce low-level memory safety.