Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Fengmin Zhu
Tutorial POPL20
Commits
78d0ea9e
Commit
78d0ea9e
authored
Jan 15, 2020
by
Robbert Krebbers
Browse files
Tweak some notations.
parent
4b4bd3fc
Changes
3
Hide whitespace changes
Inline
Side-by-side
theories/base.v
View file @
78d0ea9e
...
...
@@ -3,9 +3,9 @@ From iris.heap_lang Require Export lang notation metatheory.
(** We model type-level lambdas and applications as thunks since heap_lang does
not have them. *)
Notation
"Λ: e"
:
=
(
λ
:
<>,
e
)%
E
(
at
level
200
,
only
parsing
).
Notation
"Λ: e"
:
=
(
λ
:
<>,
e
)%
E
(
at
level
200
,
only
parsing
)
:
expr_scope
.
Notation
"Λ: e"
:
=
(
λ
:
<>,
e
)%
V
(
at
level
200
,
only
parsing
)
:
val_scope
.
Notation
"
'TApp' e
"
:
=
(
App
e
%
E
#())
(
at
level
20
0
,
only
parsing
).
Notation
"
e !
"
:
=
(
App
e
%
E
#())
(
at
level
1
0
,
only
parsing
)
:
expr_scope
.
(** We wrap unpack into an explicitly function so that we can have a nice
notation for it. *)
...
...
theories/sem_typing.v
View file @
78d0ea9e
...
...
@@ -191,12 +191,12 @@ Section typed_properties.
wp_apply
(
wp_wand
with
"(H2 [//])"
)
;
iIntros
(
v
)
"#HAB"
.
by
iApply
"HAB"
.
Qed
.
Lemma
sem_typed_tlam
Γ
e
C
:
(
∀
A
,
Γ
⊨
e
:
C
A
)
-
∗
Γ
⊨
(
λ
:
<>,
e
)
:
∀
A
,
C
A
.
Lemma
sem_typed_tlam
Γ
e
C
:
(
∀
A
,
Γ
⊨
e
:
C
A
)
-
∗
Γ
⊨
(
Λ
:
e
)
:
∀
A
,
C
A
.
Proof
.
iIntros
"#H"
(
vs
)
"!# #HΓ /="
.
wp_pures
.
iIntros
"!#"
(
A
)
"/="
.
wp_pures
.
by
iApply
(
"H"
$!
A
).
Qed
.
Lemma
sem_typed_tapp
Γ
e
C
A
:
(
Γ
⊨
e
:
∀
A
,
C
A
)
-
∗
Γ
⊨
e
#()
:
C
A
.
Lemma
sem_typed_tapp
Γ
e
C
A
:
(
Γ
⊨
e
:
∀
A
,
C
A
)
-
∗
Γ
⊨
e
!
:
C
A
.
Proof
.
iIntros
"#H"
(
vs
)
"!# #HΓ /="
.
wp_apply
(
wp_wand
with
"(H [//])"
)
;
iIntros
(
w
)
"#HB"
.
by
iApply
(
"HB"
$!
A
).
...
...
theories/typing.v
View file @
78d0ea9e
...
...
@@ -73,7 +73,7 @@ Inductive typed (Γ : gmap string ty) : expr → ty → Prop :=
Γ
⊢
ₜ
(
Λ
:
e
)
:
TForall
τ
|
TApp_typed
e
τ
τ
'
:
Γ
⊢
ₜ
e
:
TForall
τ
→
Γ
⊢
ₜ
e
#()
:
ty_subst
0
τ
'
τ
Γ
⊢
ₜ
e
!
:
ty_subst
0
τ
'
τ
|
TPack
e
τ
τ
'
:
Γ
⊢
ₜ
e
:
ty_subst
0
τ
'
τ
→
Γ
⊢
ₜ
e
:
TExist
τ
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment