Commit a7fbe118 authored by Andrew Hirsch's avatar Andrew Hirsch
Browse files

Section on equivalence reasoning.

parent 6f803820
......@@ -17,7 +17,7 @@ Module RestrictedSemantics (Import E : Expression) (Import TE : TypedExpression
Include (TypedChoreography L E TE). (* Note that a lot of results don't rely on typing, but the module system forces me to include it from the beginning *)
Include ListNotations.
Inductive RChorStep : Redex -> list Loc -> Chor -> Chor -> Prop :=
Inductive RChorStep : Redex -> list Loc -> Chor -> Chor -> Prop :=
| DoneEStep : forall (l : Loc) (e1 e2 : Expr),
ExprStep e1 e2 -> RChorStep (RDone l e1 e2) nil (Done l e1) (Done l e2)
| SendEStep : forall (l1 l2 : Loc) (B : list Loc),
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment