There was a problem fetching the pipeline mini graph.
Use Iris' iso_ofe infrastructure for types and seal off equiv and dist.
Showing
- theories/typing/fixpoint.v 11 additions, 9 deletionstheories/typing/fixpoint.v
- theories/typing/function.v 4 additions, 4 deletionstheories/typing/function.v
- theories/typing/own.v 1 addition, 1 deletiontheories/typing/own.v
- theories/typing/product.v 3 additions, 3 deletionstheories/typing/product.v
- theories/typing/shr_bor.v 2 additions, 2 deletionstheories/typing/shr_bor.v
- theories/typing/sum.v 2 additions, 2 deletionstheories/typing/sum.v
- theories/typing/type.v 161 additions, 167 deletionstheories/typing/type.v
- theories/typing/uninit.v 1 addition, 1 deletiontheories/typing/uninit.v
- theories/typing/uniq_bor.v 1 addition, 2 deletionstheories/typing/uniq_bor.v
- theories/typing/unsafe/cell.v 1 addition, 1 deletiontheories/typing/unsafe/cell.v
- theories/typing/unsafe/refcell/ref.v 2 additions, 2 deletionstheories/typing/unsafe/refcell/ref.v
- theories/typing/unsafe/refcell/refcell.v 2 additions, 2 deletionstheories/typing/unsafe/refcell/refcell.v
- theories/typing/unsafe/refcell/refmut.v 2 additions, 2 deletionstheories/typing/unsafe/refcell/refmut.v
Loading