Skip to content

GitLab

I
Iris
Commit 3fdd636a authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files
Options

Tweak decidable equality for language syntax.

parent 7b0417ad
Pipeline #94 passed with stage
    Hide whitespace changes
    Inline Side-by-side
    Showing with 5 additions and 5 deletions
    heap_lang/lang.v
    View file @ 3fdd636a
    ...@@ -51,15 +51,15 @@ Inductive val := ...@@ -51,15 +51,15 @@ Inductive val :=
    | LocV (l : loc). | LocV (l : loc).
    Global Instance base_lit_dec_eq (l1 l2 : base_lit) : Decision (l1 = l2). Global Instance base_lit_dec_eq (l1 l2 : base_lit) : Decision (l1 = l2).
    Proof. rewrite /Decision. decide equality; apply decide, _. Qed. Proof. solve_decision. Defined.
    Global Instance un_op_dec_eq (op1 op2 : un_op) : Decision (op1 = op2). Global Instance un_op_dec_eq (op1 op2 : un_op) : Decision (op1 = op2).
    Proof. rewrite /Decision. decide equality; apply decide, _. Qed. Proof. solve_decision. Defined.
    Global Instance bin_op_dec_eq (op1 op2 : bin_op) : Decision (op1 = op2). Global Instance bin_op_dec_eq (op1 op2 : bin_op) : Decision (op1 = op2).
    Proof. rewrite /Decision. decide equality; apply decide, _. Qed. Proof. solve_decision. Defined.
    Global Instance expr_dec_eq (e1 e2 : expr) : Decision (e1 = e2). Global Instance expr_dec_eq (e1 e2 : expr) : Decision (e1 = e2).
    Proof. rewrite /Decision. decide equality; apply decide, _. Qed. Proof. solve_decision. Defined.
    Global Instance val_dec_eq (v1 v2 : val) : Decision (v1 = v2). Global Instance val_dec_eq (v1 v2 : val) : Decision (v1 = v2).
    Proof. rewrite /Decision. decide equality; apply decide, _. Qed. Proof. solve_decision. Defined.
    Delimit Scope lang_scope with L. Delimit Scope lang_scope with L.
    Bind Scope lang_scope with expr val. Bind Scope lang_scope with expr 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