Skip to content
Snippets Groups Projects

Adding kinded polymorphism in types

Merged Adding kinded polymorphism in types
jonas/kinded_polymorphism into master
1 unresolved thread
Merged Jonas Kastberg requested to merge jonas/kinded_polymorphism into master
1 unresolved thread
Compare
and
8 files
+ 205
− 169
Compare changes
  • Side-by-side
  • Inline
Files
8
theories/logrel/examples/double.v
+ 1
− 1
@@ -98,7 +98,7 @@ Section double.
iSplitL; last by iApply env_ltyped_empty.
iIntros (c) "Hc".
iApply (wp_prog with "[Hc]").
{ iApply (iProto_mapsto_le _ (<??> lty_int; <??> lty_int; END)%lsty with "Hc").
{ iApply (iProto_mapsto_le _ (<??> lty_int; <??> lty_int; END)%kind with "Hc").
iApply iProto_le_recv.
iIntros "!> !> !>" (? [x ->]).
iExists _. do 2 (iSplit; [done|]).