Skip to content

Commit

Permalink
Update assets/src/semantics-of-regular-expressions/Semantics.dfy
Browse files Browse the repository at this point in the history
Co-authored-by: Rustan Leino <[email protected]>
  • Loading branch information
stefan-aws and RustanLeino authored Jan 3, 2024
1 parent 5c05c66 commit a9b8965
Showing 1 changed file with 3 additions and 1 deletion.
4 changes: 3 additions & 1 deletion assets/src/semantics-of-regular-expressions/Semantics.dfy
Original file line number Diff line number Diff line change
Expand Up @@ -108,7 +108,9 @@ module Semantics {
lemma DenotationalIsCoalgebraHomomorphism<A(!new)>()
ensures IsCoalgebraHomomorphism<A>(Denotational)
{
forall e ensures Denotational<A>(e).eps == Eps(e) {
forall e
ensures Denotational<A>(e).eps == Eps(e)
{
DenotationalIsCoalgebraHomomorphismHelper1(e);
}
forall e, a
Expand Down

0 comments on commit a9b8965

Please sign in to comment.