summaryrefslogtreecommitdiff
path: root/sec/encoding.ltx
AgeCommit message (Expand)Author
2025-05-07Give example for products and unions.Chloe Brown
2025-05-07Describe union encodings.Chloe Brown
2025-05-07Remove invalid reference to `map`.Chloe Brown
2025-05-06Give the encoding of products.Chloe Brown
2025-05-06Simplify examples and remove `map`.Chloe Brown
2025-05-06Give running examples for phase 4.Chloe Brown
2025-05-06Remove some extra whitespace.Chloe Brown
2025-05-06Remove alignment when there are intermediate linesChloe Brown
2025-05-06Justify encoding sum as tagged union.Chloe Brown
2025-05-06Explain the operators and equations on unions.Chloe Brown
2025-05-06State we encode sums as tagged unions.Chloe Brown
2025-05-02Justify why only `length` and `index`.Chloe Brown
2025-05-02Give the encoding of `match`.Chloe Brown
2025-05-02Correct phase 3 examples.Chloe Brown
2025-05-02Give the encoding of `max`.Chloe Brown
2025-05-02Foreshadow encoding of if-equal.Chloe Brown
2025-05-02Give the encoding of `snoc`.Chloe Brown
2025-05-02Give the encoding of `cons`.Chloe Brown
2025-05-02Replace `1 +` with `suc`.Chloe Brown
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-18 13:29:33 +0000