Lookup relations

def Lookup.relation {α : Type u} {Value : Type v} {Table : Type w} [Membership α Value] [Membership α Table] : Set (Value × Table)

The lookup relation. Takes in a collection of values and a table, both containers for elements of type α, and asserts that all elements in values are also in table.

Note: this generic membership typeclass allows for multiple underlying data types for Value and Table, such as List, Set, Finset, Array, Vector, etc.

Equations

• Lookup.relation = {(values, table) : Value × Table | ∀ (value : α), value ∈ values → value ∈ table}