Relation instance

Conjectura.Defs.ComputerScience.Databases.RelationInstance

/-
Copyright (c) 2026 The Conjectura Authors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: The Conjectura Authors
-/
import Mathlib.Data.Finset.Card
import Mathlib.Data.Set.Defs

/-! # Relation instance -/

namespace Conjectura.Databases

/-- A **relation instance** in the sense of the relational model: a finite set of
tuples over a fixed attribute type. This is the object every query language in
database theory manipulates. -/
abbrev RelationInstance (Attr Val : Type*) := Set (Attr → Val)

end Conjectura.Databases