Skip to content

isovector/certainty-by-construction

Repository files navigation

book

  • introduction to agda

  • proof objects

  • induction unification vs functions

  • data structures + maintaining invariants

    • linked list
    • vectors / fins for indexes
    • bst
    • heap
    • trie
  • representations matter!

    • eg matrices suck as vecs of vecs