(* iris/proofmode/classes_make.v *)
From iris.bi Require Export bi
From iris.prelude Require Import options

Class QuickAffine{PROP : bi} (P : PROP) := quick_affine : Affine P.

Global HintMode QuickAffine + ! : typeclass_instances.

Class QuickAbsorbing{PROP : bi} (P : PROP) := quick_absorbing : Absorbing P.

Global HintMode QuickAbsorbing + ! : typeclass_instances.

Class MakeEmbed{PROP PROP' : bi} `{BiEmbed PROP PROP'} (P : PROP) (Q : PROP') :=
  make_embed : ⎡P⎤ ⊣⊢ Q.

Global ArgumentsMakeEmbed {_ _ _} _%_I _%_I.

Global HintMode MakeEmbed + + + - - : typeclass_instances.

Class KnownMakeEmbed{PROP PROP' : bi} `{BiEmbed PROP PROP'} (P : PROP) (Q : PROP') :=
  #[global] known_make_embed :: MakeEmbed P Q.

Global ArgumentsKnownMakeEmbed {_ _ _} _%_I _%_I.

Global HintMode KnownMakeEmbed + + + ! - : typeclass_instances.

Class MakeSep{PROP : bi} (P Q PQ : PROP) := make_sep : P ∗ Q ⊣⊢ PQ .

Global ArgumentsMakeSep {_} _%_I _%_I _%_I.

Global HintMode MakeSep + - - - : typeclass_instances.

Class KnownLMakeSep{PROP : bi} (P Q PQ : PROP) :=
  #[global] knownl_make_sep :: MakeSep P Q PQ.

Global ArgumentsKnownLMakeSep {_} _%_I _%_I _%_I.

Global HintMode KnownLMakeSep + ! - - : typeclass_instances.

Class KnownRMakeSep{PROP : bi} (P Q PQ : PROP) :=
  #[global] knownr_make_sep :: MakeSep P Q PQ.

Global ArgumentsKnownRMakeSep {_} _%_I _%_I _%_I.

Global HintMode KnownRMakeSep + - ! - : typeclass_instances.

Class MakeAnd{PROP : bi} (P Q PQ : PROP) :=  make_and_l : P ∧ Q ⊣⊢ PQ.

Global ArgumentsMakeAnd {_} _%_I _%_I _%_I.

Global HintMode MakeAnd + - - - : typeclass_instances.

Class KnownLMakeAnd{PROP : bi} (P Q PQ : PROP) :=
  #[global] knownl_make_and :: MakeAnd P Q PQ.

Global ArgumentsKnownLMakeAnd {_} _%_I _%_I _%_I.

Global HintMode KnownLMakeAnd + ! - - : typeclass_instances.

Class KnownRMakeAnd{PROP : bi} (P Q PQ : PROP) :=
  #[global] knownr_make_and :: MakeAnd P Q PQ.

Global ArgumentsKnownRMakeAnd {_} _%_I _%_I _%_I.

Global HintMode KnownRMakeAnd + - ! - : typeclass_instances.

Class MakeOr{PROP : bi} (P Q PQ : PROP) := make_or_l : P ∨ Q ⊣⊢ PQ.

Global ArgumentsMakeOr {_} _%_I _%_I _%_I.

Global HintMode MakeOr + - - - : typeclass_instances.

Class KnownLMakeOr{PROP : bi} (P Q PQ : PROP) :=
  #[global] knownl_make_or :: MakeOr P Q PQ.

Global ArgumentsKnownLMakeOr {_} _%_I _%_I _%_I.

Global HintMode KnownLMakeOr + ! - - : typeclass_instances.

Class KnownRMakeOr{PROP : bi} (P Q PQ : PROP) := #[global] knownr_make_or :: MakeOr P Q PQ.

Global ArgumentsKnownRMakeOr {_} _%_I _%_I _%_I.

Global HintMode KnownRMakeOr + - ! - : typeclass_instances.

Class MakeAffinely{PROP : bi} (P Q : PROP) :=
  make_affinely : <affine> P ⊣⊢ Q.

Global ArgumentsMakeAffinely {_} _%_I _%_I.

Global HintMode MakeAffinely + - - : typeclass_instances.

Class KnownMakeAffinely{PROP : bi} (P Q : PROP) :=
  #[global] known_make_affinely :: MakeAffinely P Q.

Global ArgumentsKnownMakeAffinely {_} _%_I _%_I.

Global HintMode KnownMakeAffinely + ! - : typeclass_instances.

Class MakeIntuitionistically{PROP : bi} (P Q : PROP) :=
  make_intuitionistically : □ P ⊣⊢ Q.

Global ArgumentsMakeIntuitionistically {_} _%_I _%_I.

Global HintMode MakeIntuitionistically + - - : typeclass_instances.

Class KnownMakeIntuitionistically{PROP : bi} (P Q : PROP) :=
  #[global] known_make_intuitionistically :: MakeIntuitionistically P Q.

Global ArgumentsKnownMakeIntuitionistically {_} _%_I _%_I.

Global HintMode KnownMakeIntuitionistically + ! - : typeclass_instances.

Class MakeAbsorbingly{PROP : bi} (P Q : PROP) :=
  make_absorbingly : <absorb> P ⊣⊢ Q.

Global ArgumentsMakeAbsorbingly {_} _%_I _%_I.

Global HintMode MakeAbsorbingly + - - : typeclass_instances.

Class KnownMakeAbsorbingly{PROP : bi} (P Q : PROP) :=
  #[global] known_make_absorbingly :: MakeAbsorbingly P Q.

Global ArgumentsKnownMakeAbsorbingly {_} _%_I _%_I.

Global HintMode KnownMakeAbsorbingly + ! - : typeclass_instances.

Class MakePersistently{PROP : bi} (P Q : PROP) :=
  make_persistently : <pers> P ⊣⊢ Q.

Global ArgumentsMakePersistently {_} _%_I _%_I.

Global HintMode MakePersistently + - - : typeclass_instances.

Class KnownMakePersistently{PROP : bi} (P Q : PROP) :=
  #[global] known_make_persistently :: MakePersistently P Q.

Global ArgumentsKnownMakePersistently {_} _%_I _%_I.

Global HintMode KnownMakePersistently + ! - : typeclass_instances.

Class MakeLaterN{PROP : bi} (n : nat) (P lP : PROP) :=
  make_laterN : ▷^n P ⊣⊢ lP.

Global ArgumentsMakeLaterN {_} _%_nat _%_I _%_I.

Global HintMode MakeLaterN + + - - : typeclass_instances.

Class KnownMakeLaterN{PROP : bi} (n : nat) (P lP : PROP) :=
  #[global] known_make_laterN :: MakeLaterN n P lP.

Global ArgumentsKnownMakeLaterN {_} _%_nat _%_I _%_I.

Global HintMode KnownMakeLaterN + + ! - : typeclass_instances.

Class MakeExcept0{PROP : bi} (P Q : PROP) :=
  make_except_0 : ◇ P ⊣⊢ Q.

Global ArgumentsMakeExcept0 {_} _%_I _%_I.

Global HintMode MakeExcept0 + - - : typeclass_instances.

Class KnownMakeExcept0{PROP : bi} (P Q : PROP) :=
  #[global] known_make_except_0 :: MakeExcept0 P Q.

Global ArgumentsKnownMakeExcept0 {_} _%_I _%_I.

Global HintMode KnownMakeExcept0 + ! - : typeclass_instances.