Variable: Named Causal Atoms (V2)

The default vertex carrier for theory-side SEMs. A Variable is just a named atom; semantic content lives in mechanisms attached to vertices, not in the variable itself.

CausalGraph V is generic in the vertex type V; Variable is the canonical default. Use directly when you don't need polymorphism.

structure Core.Causal.Variable : Type

A variable in a causal model: a named atom. Semantic content lives in the Mechanism attached to a vertex, not in the variable itself.

BEq/LawfulBEq are auto-derived from DecidableEq via instBEqOfDecidableEq.

• name : String

def Core.Causal.instDecidableEqVariable.decEq (x✝ x✝¹ : Variable) : Decidable (x✝ = x✝¹)

Equations

• Core.Causal.instDecidableEqVariable.decEq { name := a } { name := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Core.Causal.instDecidableEqVariable : DecidableEq Variable

Equations

• Core.Causal.instDecidableEqVariable = Core.Causal.instDecidableEqVariable.decEq

@[implicit_reducible]

instance Core.Causal.instHashableVariable : Hashable Variable

Equations

• Core.Causal.instHashableVariable = { hash := Core.Causal.instHashableVariable.hash }

def Core.Causal.instHashableVariable.hash : Variable → UInt64

Equations

• Core.Causal.instHashableVariable.hash { name := a } = mixHash 0 (hash a)

def Core.Causal.instReprVariable.repr : Variable → ℕ → Std.Format

Equations

• Core.Causal.instReprVariable.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "name" ++ Std.Format.text " := " ++ (Std.Format.nest 8 (repr x✝.name)).group) " }"

@[implicit_reducible]

instance Core.Causal.instReprVariable : Repr Variable

Equations

• Core.Causal.instReprVariable = { reprPrec := Core.Causal.instReprVariable.repr }

@[implicit_reducible]

instance Core.Causal.instInhabitedVariable : Inhabited Variable

Equations

• Core.Causal.instInhabitedVariable = { default := Core.Causal.instInhabitedVariable.default }

def Core.Causal.instInhabitedVariable.default : Variable

Equations

• Core.Causal.instInhabitedVariable.default = { name := default }

@[implicit_reducible]

instance Core.Causal.instToStringVariable : ToString Variable

Equations

• Core.Causal.instToStringVariable = { toString := fun (v : Core.Causal.Variable) => v.name }