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

Attempt at proving for arbitrary operators

thm3

Proving for arbitrary operators using axioms

genPrefixSumInstance

prefixSum

yices1029

yicesSMT09

Inspecting symbolic traces

ladnerFischerTrace

scanlTrace