Make [ELCtx_Alive] a coercion.
I needed to uncurry the [fn] type, so that type inference infers first that the generalized variables are lifetimes, before typechecking the external lifetime contexts.
parent
094097c8
No related branches found
No related tags found
Showing
- theories/typing/examples/get_x.v 1 addition, 1 deletiontheories/typing/examples/get_x.v
- theories/typing/examples/unbox.v 1 addition, 1 deletiontheories/typing/examples/unbox.v
- theories/typing/function.v 125 additions, 111 deletionstheories/typing/function.v
- theories/typing/lft_contexts.v 8 additions, 8 deletionstheories/typing/lft_contexts.v
- theories/typing/lib/cell.v 3 additions, 3 deletionstheories/typing/lib/cell.v
- theories/typing/lib/fake_shared_box.v 2 additions, 3 deletionstheories/typing/lib/fake_shared_box.v
- theories/typing/lib/option.v 1 addition, 1 deletiontheories/typing/lib/option.v
- theories/typing/lib/refcell/ref_code.v 7 additions, 9 deletionstheories/typing/lib/refcell/ref_code.v
- theories/typing/lib/refcell/refcell_code.v 5 additions, 9 deletionstheories/typing/lib/refcell/refcell_code.v
- theories/typing/lib/refcell/refmut_code.v 9 additions, 12 deletionstheories/typing/lib/refcell/refmut_code.v
- theories/typing/lib/rwlock/rwlock_code.v 5 additions, 9 deletionstheories/typing/lib/rwlock/rwlock_code.v
- theories/typing/lib/rwlock/rwlockreadguard_code.v 3 additions, 4 deletionstheories/typing/lib/rwlock/rwlockreadguard_code.v
- theories/typing/lib/rwlock/rwlockwriteguard_code.v 7 additions, 7 deletionstheories/typing/lib/rwlock/rwlockwriteguard_code.v
- theories/typing/lib/spawn.v 1 addition, 2 deletionstheories/typing/lib/spawn.v
Loading
Please register or sign in to comment