/agdademo

"Proving Theorems About Functional Programs" code and patter

Primary LanguageAgda

  • foldrl-simpler.agda

    all the proofs that i did in RG, but just as agda without much explanation about what's going on. it also includes a proof that if you have an f at A -> A -> A that's associative and commutative, that implies that it has the Δ property

  • foldrl.agda

    the same whole work up, but with the version of the proof that invoves rev before I noticed that I didn't need to make the detour

  • live-23-feb.agda

    what I wrote live in RG

  • patter.md

    the script / notes that i worked up for myself in getting ready for RG.

  • readme.md

    this file