Commit 35bba4ed authored by Robbert Krebbers's avatar Robbert Krebbers

Some canonical structure instances for heap_lang.

parent 9fb4882f
Pipeline #1412 passed with stage
From iris.program_logic Require Export ectx_language ectxi_language.
From iris.algebra Require Export cofe.
From iris.prelude Require Export strings.
From iris.prelude Require Import gmap.
......@@ -508,6 +509,10 @@ Defined.
Instance expr_inhabited X : Inhabited (expr X) := populate (Lit LitUnit).
Instance val_inhabited : Inhabited val := populate (LitV LitUnit).
Canonical Structure stateC := leibnizC state.
Canonical Structure valC := leibnizC val.
Canonical Structure exprC X := leibnizC (expr X).
End heap_lang.
(** Language *)
......
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