bi.v 528 Bytes
Newer Older
1
From iris.bi Require Export derived_laws derived_laws_later big_op.
2
From iris.bi Require Export updates internal_eq plainly embedding.
Ralf Jung's avatar
Ralf Jung committed
3
From iris.prelude Require Import options.
Robbert Krebbers's avatar
Robbert Krebbers committed
4
5

Module Import bi.
6
7
8
9
10
11
  (** Get universes into the desired scope *)
  Universe Logic.
  Constraint Logic = bi.interface.universes.Logic.
  Universe Quant.
  Constraint Quant = bi.interface.universes.Quant.
  (** Get other symbols into the desired scope *)
Robbert Krebbers's avatar
Robbert Krebbers committed
12
  Export bi.interface.bi.
13
14
  Export bi.derived_laws.bi.
  Export bi.derived_laws_later.bi.
Robbert Krebbers's avatar
Robbert Krebbers committed
15
End bi.