def Iris.Std.bigOp {PROP : Type u_1} (f : PROP → PROP → PROP) (unit : PROP) : List PROP → PROP

Fold a binary operator f over a list of PROPs. If the list is empty, unit is returned.

Equations

• Iris.Std.bigOp f unit [] = unit
• Iris.Std.bigOp f unit [P] = P
• Iris.Std.bigOp f unit (P :: Ps) = f P (Iris.Std.bigOp f unit Ps)

class Iris.Std.LawfulBigOp {PROP : Sort u_1} (f : PROP → PROP → PROP) (unit : outParam PROP) (eq : outParam (PROP → PROP → Prop)) : Prop

• refl {a : PROP} : eq a a
• symm {a b : PROP} : eq a b → eq b a
• trans {a b c : PROP} : eq a b → eq b c → eq a c
• comm {a b : PROP} : eq (f a b) (f b a)
• assoc {a b c : PROP} : eq (f (f a b) c) (f a (f b c))
• left_id {a : PROP} : eq (f unit a) a
• congr_l {a a' b : PROP} : eq a a' → eq (f a b) (f a' b)

theorem Iris.Std.LawfulBigOp.right_id {PROP : Sort u_1} {f : PROP → PROP → PROP} {unit : PROP} {eq : PROP → PROP → Prop} {a : PROP} [LawfulBigOp f unit eq] : eq (f a unit) a

theorem Iris.Std.LawfulBigOp.congr_r {PROP : Sort u_1} {f : PROP → PROP → PROP} {unit : PROP} {eq : PROP → PROP → Prop} {b b' a : PROP} [LawfulBigOp f unit eq] (h : eq b b') : eq (f a b) (f a b')

theorem Iris.Std.bigOp_nil {PROP : Type u_1} {f : PROP → PROP → PROP} {unit : PROP} : bigOp f unit [] = unit

theorem Iris.Std.bigOp_cons {PROP : Type u_1} {eq : PROP → PROP → Prop} {P : PROP} {Ps : List PROP} {f : PROP → PROP → PROP} {unit : PROP} [LawfulBigOp f unit eq] : eq (bigOp f unit (P :: Ps)) (f P (bigOp f unit Ps))