Skip to content
Snippets Groups Projects
Commit 0975c0ac authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Remove deadcode `symbol_ctx`.

parent c54cc72f
No related branches found
No related tags found
No related merge requests found
Pipeline #16160 passed
Stage: build
Hide whitespace changes
Inline Side-by-side
theories/logrel_heaplang/lib/symbol_adt.v
+ 0
− 3
View file @ 0975c0ac
...@@ -65,9 +65,6 @@ Section ltyped_symbol_adt. ...@@ -65,9 +65,6 @@ Section ltyped_symbol_adt.
Definition symbol_inv (γ : gname) (l : loc) : iProp Σ := Definition symbol_inv (γ : gname) (l : loc) : iProp Σ :=
(∃ n : nat, l ↦ #n ∗ counter γ n)%I. (∃ n : nat, l ↦ #n ∗ counter γ n)%I.
Definition symbol_ctx (γ : gname) (l : loc) : iProp Σ :=
inv symbol_adtN (symbol_inv γ l).
Definition lty_symbol (γ : gname) : lty Σ := Lty (λ w, Definition lty_symbol (γ : gname) : lty Σ := Lty (λ w,
∃ n : nat, ⌜w = #n⌝ ∧ symbol γ n)%I. ∃ n : nat, ⌜w = #n⌝ ∧ symbol γ n)%I.
......
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