Opened 11 years ago

Last modified 11 years ago

#1 new lemma

Lifting doesn't introduce capabilities.

Reported by: benl Owned by: benl
Priority: normal Milestone:
Component: SystemF2Effect Version:
Keywords: Cc:

Description

In WeakKiEnv / Case !XUse

     ~ mentionsCapT (TyCapRegion n) t1
------------------------------------------
 ~ mentionsCapT (TyCapRegion n) (liftTT 1 ix t1)

Change History (1)

comment:1 Changed 11 years ago by benl

Summary: Lemma: Lifting doesn't introduce capabilities. → Lifting doesn't introduce capabilities.
Type: defect → lemma
Note: See TracTickets for help on using tickets.