Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

itree_iter respects wbisim + strong bisimulation #1152

Merged
merged 11 commits into from
Oct 9, 2023

Conversation

Plisp
Copy link
Contributor

@Plisp Plisp commented Oct 5, 2023

added itree_bind_thm simp + itree_iter respecting pointwise wbisim proof

@Plisp Plisp changed the title itree_iter respects weak bisimilarity itree_iter respects wbisim + strong bisimulation Oct 7, 2023
src/coalgebras/itreeTauScript.sml Outdated Show resolved Hide resolved
@mn200 mn200 removed the request for review from IlmariReissumies October 9, 2023 06:39
@mn200 mn200 marked this pull request as ready for review October 9, 2023 06:39
@mn200 mn200 merged commit 4e98178 into HOL-Theorem-Prover:develop Oct 9, 2023
2 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants