base_logic.v 509 Bytes
Newer Older
1
From iris.base_logic Require Export derived.
2
Set Default Proof Using "Type*".
3

4 5 6 7
Module Import uPred.
  Export upred.uPred.
  Export primitive.uPred.
  Export derived.uPred.
8 9 10 11 12 13 14 15 16
End uPred.

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