summaryrefslogtreecommitdiff
path: root/sec/encoding.ltx
AgeCommit message (Expand)Author
2025-05-02Give the encoding of nil.Chloe Brown
2025-04-30Give phase 3 examples.Chloe Brown
2025-04-30Fix typoChloe Brown
2025-04-30State we encode lists using eliminators.Chloe Brown
2025-04-30Add headings for each phase.Chloe Brown
2025-04-30Justify adding the `match` operator.Chloe Brown
2025-04-30Justify the `index` operator.Chloe Brown
2025-04-30Correct TODO list.Chloe Brown
2025-04-30Make phase 2 `balanced` use `index`.Chloe Brown
2025-04-29Give (weak) justification for adding `snoc`.Chloe Brown
2025-04-29Provide (weak) justification for `max`.Chloe Brown
2025-04-29Fix pseudocode.Chloe Brown
2025-04-29Move figure before reference.Chloe Brown
2025-04-29Give the encoding for fold.Chloe Brown
2025-04-29Give the encoding of roll.Chloe Brown
2025-04-29Update examples for end of phase 2.Chloe Brown
2025-04-29Explain why we used natural-list indices.Chloe Brown
2025-04-29Explain why we use a heap encoding.Chloe Brown
2025-04-25Give examples for phase 1.Chloe Brown
2025-04-25Describe encoding of inductive types.Chloe Brown
2025-04-24Describe distrib.Chloe Brown
2025-04-24Describe the roll' operator.Chloe Brown
2025-04-24Describe why roll is hard to encode.Chloe Brown
2025-04-23Current state of affairs.Chloe Brown
generated by cgit v1.2.3 (git 2.49.0) at 2025-07-17 13:39:02 +0000