Skip to content
Snippets Groups Projects
Commit bb35dbf5 authored by Ralf Jung's avatar Ralf Jung
Browse files

solve_inG ftw

parent 04386c1c
No related branches found
No related tags found
No related merge requests found
Pipeline #
Hide whitespace changes
Inline Side-by-side
theories/typing/adequacy.v
+ 1
− 7
View file @ bb35dbf5
...@@ -18,13 +18,7 @@ Class typePreG Σ := PreTypeG { ...@@ -18,13 +18,7 @@ Class typePreG Σ := PreTypeG {
Definition typeΣ : gFunctors := Definition typeΣ : gFunctors :=
#[heapΣ; lftΣ; na_invΣ; GFunctor (constRF fracR)]. #[heapΣ; lftΣ; na_invΣ; GFunctor (constRF fracR)].
Instance subG_typePreG {Σ} : subG typeΣ Σ → typePreG Σ. Instance subG_typePreG {Σ} : subG typeΣ Σ → typePreG Σ.
Proof. Proof. solve_inG. Qed.
split.
- apply subG_heapPreG. solve_inG.
- apply subG_lftPreG. solve_inG.
- solve_inG.
- solve_inG.
Qed.
Section type_soundness. Section type_soundness.
Definition exit_cont : val := λ: [<>], #(). Definition exit_cont : val := λ: [<>], #().
......
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