Commit 10c5a51c authored by David Swasey's avatar David Swasey
Browse files

Eliminate an unnecessary typeclass.

parent b1e67232
......@@ -129,8 +129,8 @@ Section ectx_language.
Canonical Structure ectx_lang : language := Language ectx_lang_mixin.
Class HeadAtomic (s : stuckness) (e : expr Λ) : Prop :=
head_atomic σ e' σ' efs :
Definition HeadAtomic (s : stuckness) (e : expr Λ) : Prop :=
σ e' σ' efs,
head_step e σ e' σ' efs
if s is not_stuck then irreducible e' σ' else is_Some (to_val e').
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