Commit 59999b0f authored by Robbert Krebbers's avatar Robbert Krebbers

Make language argument of `LanguageCtx` implicit.

It can be infered now.
parent 347cd0f5
......@@ -176,7 +176,7 @@ Section ectx_language.
Qed.
(* Every evaluation context is a context. *)
Global Instance ectx_lang_ctx K : LanguageCtx _ (fill K).
Global Instance ectx_lang_ctx K : LanguageCtx (fill K).
Proof.
split; simpl.
- eauto using fill_not_val.
......
......@@ -114,8 +114,8 @@ Section ectxi_language.
intros []%eq_None_not_Some. eapply fill_val, Hsub. by rewrite /= fill_app.
Qed.
Global Instance ectxi_lang_ctx_item Ki : LanguageCtx _ (fill_item Ki).
Proof. change (LanguageCtx ectxi_lang (fill [Ki])). apply _. Qed.
Global Instance ectxi_lang_ctx_item Ki : LanguageCtx (fill_item Ki).
Proof. change (LanguageCtx (fill [Ki])). apply _. Qed.
End ectxi_language.
Arguments fill {_} _ _%E.
......
......@@ -39,7 +39,7 @@ Canonical Structure exprC Λ := leibnizC (expr Λ).
Definition cfg (Λ : language) := (list (expr Λ) * state Λ)%type.
Class LanguageCtx (Λ : language) (K : expr Λ expr Λ) := {
Class LanguageCtx {Λ : language} (K : expr Λ expr Λ) := {
fill_not_val e :
to_val e = None to_val (K e) = None;
fill_step e1 σ1 e2 σ2 efs :
......@@ -50,7 +50,7 @@ Class LanguageCtx (Λ : language) (K : expr Λ → expr Λ) := {
e2', e2 = K e2' prim_step e1' σ1 e2' σ2 efs
}.
Instance language_ctx_id Λ : LanguageCtx Λ id.
Instance language_ctx_id Λ : LanguageCtx (@id (expr Λ)).
Proof. constructor; naive_solver. Qed.
Section language.
......
......@@ -174,7 +174,7 @@ Proof.
iSplitR "H"; last iExact "H". iIntros (v) "H". by iApply "H".
Qed.
Lemma wp_bind K `{!LanguageCtx Λ K} E e Φ :
Lemma wp_bind K `{!LanguageCtx K} E e Φ :
WP e @ E {{ v, WP K (of_val v) @ E {{ Φ }} }} WP K e @ E {{ Φ }}.
Proof.
iIntros "H". iLöb as "IH" forall (E e Φ). rewrite wp_unfold /wp_pre.
......@@ -189,7 +189,7 @@ Proof.
by iApply "IH".
Qed.
Lemma wp_bind_inv K `{!LanguageCtx Λ K} E e Φ :
Lemma wp_bind_inv K `{!LanguageCtx K} E e Φ :
WP K e @ E {{ Φ }} WP e @ E {{ v, WP K (of_val v) @ E {{ Φ }} }}.
Proof.
iIntros "H". iLöb as "IH" forall (E e Φ). rewrite !wp_unfold /wp_pre.
......
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