diff options
author | Chloe Brown <chloe.brown.00@outlook.com> | 2025-04-29 18:06:58 +0100 |
---|---|---|
committer | Chloe Brown <chloe.brown.00@outlook.com> | 2025-04-29 18:06:58 +0100 |
commit | 8c5d117581230548fc23110d2d6095762306adf7 (patch) | |
tree | 161efd1f8eae74a13bc17ec2d3dfafd89069ca2d | |
parent | 2d033819b2666f92e90a91d8284768097fa0ee79 (diff) |
Fix pseudocode.
- Make `arb` a keyword.
- Correct argument order to `map`.
-rw-r--r-- | lexer.py | 12 | ||||
-rw-r--r-- | sec/encoding.ltx | 4 |
2 files changed, 13 insertions, 3 deletions
@@ -9,7 +9,17 @@ class SystemTLexer(OcamlLexer): aliases = ['syst'] filenames = ['*.syst'] - EXTRA_KEYWORDS = ['primrec', 'fold', 'foldmatch', 'roll', 'roll2'] + EXTRA_KEYWORDS = [ + 'arb', + 'arb)', + 'fold', + 'foldmatch', + 'map', + 'max', + 'primrec', + 'roll', + 'roll2', + ] def get_tokens_unprocessed(self, text): for index, token, value in OcamlLexer.get_tokens_unprocessed(self, text): diff --git a/sec/encoding.ltx b/sec/encoding.ltx index 8de40c4..dc3f8c8 100644 --- a/sec/encoding.ltx +++ b/sec/encoding.ltx @@ -158,7 +158,7 @@ index of the given child. More formally, we encode the type \(\mu X. A\) as \(\nat \times (\mathsf{List}~\nat \to \sub{A}{X/\nat})\), recursively encoding \(A\). We present the encoding of \roll*{} and \foldkw{} in -\cref{fig:phase-2-encode}. +\cref{fig:phase-2-encode}. \TODO{ \begin{itemize} @@ -194,7 +194,7 @@ let compose (depth, heap) = let go = primrec depth with Zero => arb | Suc ih => fun index => - let x = map (heap index) (fun x => ih (snoc xs x)) in + let x = map (fun x => ih (snoc xs x)) (heap index) in match x with Leaf f => f | Branch (f, g) => fun x => f (g x) |