-
Notifications
You must be signed in to change notification settings - Fork 2
Open
Description
Currently, we have code like:
if eq(length(M), |nonce|) then
if eq(length(A), |nonce|) then
if eq(length(B), |nonce|) then
case x1
| mA2_enc _ => ()
| mA1_enc x1' =>
(case dec(kA, x1')
| None => ()
| Some resA =>
unpack j1, resA' = resA in
unpack j2, resA'' = resA' in
(case resA''
| mA1 msg1A => ...
| mA2 _ => ...))
Aside from the nested equality checks, we also want better syntax for nested case expressions, and nested unpacks.
Perhaps something like:
(mA1_enc x1') =? x1 in
(Some ResA) =? dec(kA, x1') in
...
where the semantics of =? is to return () if the pattern match fails. (Or, perhaps if we return an option, to return None).
A Rust-style if let operation would work well too.
Reactions are currently unavailable
Metadata
Metadata
Assignees
Labels
No labels