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
7c00a718
Commit
7c00a718
authored
Jan 16, 2020
by
Robbert Krebbers
Browse files
Better notation for type application.
parent
7f235325
Changes
4
Hide whitespace changes
Inline
Side-by-side
theories/base.v
View file @
7c00a718
...
...
@@ -6,7 +6,7 @@ From iris.heap_lang.lib Require Export assert.
not have them. *)
Notation
"Λ: e"
:
=
(
λ
:
<>,
e
)%
E
(
at
level
200
,
only
parsing
)
:
expr_scope
.
Notation
"Λ: e"
:
=
(
λ
:
<>,
e
)%
V
(
at
level
200
,
only
parsing
)
:
val_scope
.
Notation
"e
!
"
:
=
(
App
e
%
E
#())
(
at
level
10
,
only
parsing
)
:
expr_scope
.
Notation
"e
'<_>'
"
:
=
(
App
e
%
E
#())
(
at
level
10
,
only
parsing
)
:
expr_scope
.
(** We wrap unpack into an explicitly function so that we can have a nice
notation for it. *)
...
...
theories/compatibility.v
View file @
7c00a718
...
...
@@ -92,7 +92,7 @@ Section compatibility.
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/parametricity.v
View file @
7c00a718
...
...
@@ -8,7 +8,7 @@ Section parametricity.
Lemma
exercise5
`
{!
heapPreG
Σ
}
e
(
v
:
val
)
σ
w
es
σ
'
:
(
∀
`
{
heapG
Σ
},
∅
⊨
e
:
∀
A
,
A
→
A
)
→
rtc
erased_step
([
e
!
v
]%
E
,
σ
)
(
of_val
w
::
es
,
σ
'
)
→
w
=
v
.
rtc
erased_step
([
e
<
_
>
v
]%
E
,
σ
)
(
of_val
w
::
es
,
σ
'
)
→
w
=
v
.
(* REMOVE *)
Proof
.
intros
He
.
apply
sem_gen_type_safety
with
(
φ
:
=
λ
u
,
u
=
v
)=>
?.
...
...
@@ -27,10 +27,10 @@ Section parametricity.
Lemma
exercise6
`
{!
heapPreG
Σ
}
e
(
v
:
val
)
σ
w
es
σ
'
:
(
∀
`
{
heapG
Σ
},
∅
⊨
e
:
∀
A
,
A
)
→
¬
rtc
erased_step
([
e
!]%
E
,
σ
)
(
of_val
w
::
es
,
σ
'
).
rtc
erased_step
([
e
<
_
>]%
E
,
σ
)
(
of_val
w
::
es
,
σ
'
)
→
False
.
(* REMOVE *)
Proof
.
intros
He
.
unfold
not
.
change
False
with
((
λ
_
,
False
)
w
).
apply
sem_gen_type_safety
with
(
φ
:
=
λ
_
,
False
)=>
?.
exists
(
exercise6_sem_ty
Σ
).
split
.
...
...
theories/typing.v
View file @
7c00a718
...
...
@@ -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