Commit e1c5e026 authored by Ralf Jung's avatar Ralf Jung
Browse files

disambiguate an mret

Thanks to Paolo G. Giarrusso
parent 2959900d
......@@ -151,7 +151,7 @@ Module interp_monad.
Proof. by inversion 1. Qed.
Lemma mret_inv {A} (v: A) s v' s' :
mret v s = (inl v', s') v = v' s = s'.
mret (M := InterpretM) v s = (inl v', s') v = v' s = s'.
Proof. by inversion 1. Qed.
Lemma interp_bind_inv A B (x: InterpretM A) (f: A InterpretM B) r s s' :
......
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