Commit c6673311 authored by Jonas Kastberg's avatar Jonas Kastberg

Nits

parent 0942c365
......@@ -28,7 +28,7 @@ Definition lty_forall `{heapG Σ} {k} (C : lty Σ k → ltty Σ) : ltty Σ :=
Ltty (λ w, A, WP w #() {{ ltty_car (C A) }})%I.
Definition lty_exist {Σ k} (C : lty Σ k ltty Σ) : ltty Σ :=
Ltty (λ w, A, ltty_car (C A) w)%I.
Definition lty_texist {Σ} {TT : ktele Σ} (C : kt ltty Σ) : ltty Σ :=
Definition lty_texist {Σ} {kt : ktele Σ} (C : ltys kt ltty Σ) : ltty Σ :=
ktele_fold (@lty_exist Σ) (λ x, x) (ktele_bind C).
Definition lty_ref_mut `{heapG Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w,
......
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