Skip to content

Commit

Permalink
Update plutus-metatheory/src/VerifiedCompilation/UCaseOfCase.lagda.md
Browse files Browse the repository at this point in the history
Co-authored-by: effectfully <effectfully@gmail.com>
  • Loading branch information
ramsay-t and effectfully committed May 3, 2024
1 parent 5883687 commit 5ca05ab
Showing 1 changed file with 1 addition and 1 deletion.
Original file line number Diff line number Diff line change
Expand Up @@ -82,7 +82,7 @@ This can just traverse the ASTs applying the constructors from the transition re
We can show that this translation never alters the semantics of the statement. This is shown
in terms of the CEK machine evaluation. Since it is a simple re-arrangement of the syntax, it
isn't a refinement argument - the state before and after the operation is the same type, and is
unaltered buy the syntax re-arrangement.
unaltered by the syntax re-arrangement.

This does rely on the encoding of the semantics of `IfThenElse` in the CEK module, since we
need to show that the effective list of cases is the same as it would have been without the re-arrangement.
Expand Down

0 comments on commit 5ca05ab

Please sign in to comment.