Data.SBV.Examples.BitPrecise.PrefixSum

Formalizing power-lists

type PowerList a

tiePL

zipPL

unzipPL

Reference prefix-sum implementation

ps

The Ladner-Fischer parallel version

lf

Sample proofs for concrete operators

flIsCorrect

thm1

thm2

Inspecting symbolic traces

ladnerFischerTrace

scanlTrace