Commit 46f8eed8 authored by Robbert Krebbers's avatar Robbert Krebbers

Turn a ~ into a ¬.

parent 2521b1a9
...@@ -35,7 +35,7 @@ Section language. ...@@ -35,7 +35,7 @@ Section language.
Definition reducible (e : expr Λ) (σ : state Λ) := Definition reducible (e : expr Λ) (σ : state Λ) :=
e' σ' efs, prim_step e σ e' σ' efs. e' σ' efs, prim_step e σ e' σ' efs.
Definition irreducible (e : expr Λ) (σ : state Λ) := Definition irreducible (e : expr Λ) (σ : state Λ) :=
e' σ' efs, ~prim_step e σ e' σ' efs. e' σ' efs, ¬prim_step e σ e' σ' efs.
Definition atomic (e : expr Λ) : Prop := Definition atomic (e : expr Λ) : Prop :=
σ e' σ' efs, prim_step e σ e' σ' efs irreducible e' σ'. σ e' σ' efs, prim_step e σ e' σ' efs irreducible e' σ'.
Inductive step (ρ1 ρ2 : cfg Λ) : Prop := Inductive step (ρ1 ρ2 : cfg Λ) : Prop :=
......
Markdown is supported
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