summaryrefslogtreecommitdiff
path: root/agda-helium.agda-lib
diff options
context:
space:
mode:
authorGreg Brown <greg.brown@cl.cam.ac.uk>2022-03-19 13:28:42 +0000
committerGreg Brown <greg.brown@cl.cam.ac.uk>2022-03-19 13:53:40 +0000
commit535e4297a08c626d0e2e1923914727f914b8c9bd (patch)
tree10e9b728083c4c69b80c3a07c4e68bfa025519c8 /agda-helium.agda-lib
parent78aad93db3d7029e0a9a8517a2db92533fd1f401 (diff)
Modify pseudocode definition.
This change makes the following changes to the definition of pseudocode: - Add a separate type `bit` for single-bit values. - Change `var` and `state` to take `Fin`s instead of bounded naturals. - Make `[_]` and `unbox` work for any sliced type. - Generalise `_:_` and `slice` into `splice` and `cut` respectively, making the two new operations inverses. - Replace `tup` with `nil` and `cons` for building tuples. - Add destructors `head` and `tail` for tuple types. - Make function and procedure calls take a vector of arguments instead of a tuple. - Introduce an `if_then_` expression for if statements with a trivial else branch.
Diffstat (limited to 'agda-helium.agda-lib')
0 files changed, 0 insertions, 0 deletions