A Foldable typeclass for big operators

A small typeclass abstracting collections that can be folded with a commutative-associative operation, used to give big-conjunction and big-disjunction TLA operators a uniform definition.

class TLA.Foldable (c : Type u → Type v) : Type (max (max (u + 1) v) (w + 1))

A customized typeclass to express structures that can be folded upon.

• fold {α : Type u} {β : Type w} (op : β → β → β) [Std.Commutative op] [Std.Associative op] (b : β) (f : α → β) (s : c α) : β

  Fold a finite collection with a commutative-associative operation.

@[implicit_reducible]

instance TLA.instFoldableList : Foldable List

Equations

• One or more equations did not get rendered due to their size.

theorem TLA.Foldable.list_index_form_change {α : Type u} {β : Type w} (op : β → β → β) [inst1 : Std.Commutative op] [inst2 : Std.Associative op] (b : β) (f : α → β) (l : List α) : fold op b f l = fold op b (fun (x : Fin l.length) => f l[x]) (List.finRange l.length)

Folding over a list equals folding over its positional re-indexing through List.finRange.