Commit c01717fb authored by Robbert Krebbers's avatar Robbert Krebbers

Prove `LanguageCtx Λ id`.

parent 10830bed
......@@ -40,6 +40,9 @@ Class LanguageCtx (Λ : language) (K : expr Λ → expr Λ) := {
e2', e2 = K e2' prim_step e1' σ1 e2' σ2 efs
}.
Instance language_ctx_id Λ : LanguageCtx Λ id.
Proof. constructor; naive_solver. Qed.
Section language.
Context {Λ : language}.
Implicit Types v : val Λ.
......
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