bi.v 535 Bytes
Newer Older
1
From iris.bi Require Export derived_laws big_op updates.
Robbert Krebbers's avatar
Robbert Krebbers committed
2
3
4
5
Set Default Proof Using "Type".

Module Import bi.
  Export bi.interface.bi.
6
  Export bi.derived_laws.bi.
Robbert Krebbers's avatar
Robbert Krebbers committed
7
8
9
10
11
12
13
14
15
16
17
18
19
  Export bi.big_op.bi.
End bi.

(* Hint DB for the logic *)
Hint Resolve pure_intro.
Hint Resolve or_elim or_intro_l' or_intro_r' : BI.
Hint Resolve and_intro and_elim_l' and_elim_r' : BI.
Hint Resolve persistently_mono : BI.
Hint Resolve sep_elim_l sep_elim_r sep_mono : BI.
Hint Immediate True_intro False_elim : BI.
(*
Hint Immediate iff_refl internal_eq_refl' : BI.
*)