-
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
isovector/certainty-by-construction
Folders and files
| Name | Name | Last commit date | ||
|---|---|---|---|---|