kdrag.property

Generic properties like associativity, commutativity, idempotence, etc.

Classes

Antisymm(*args, **kwargs)	forall x y, rel(x, y) and rel(y, x) implies x = y
Assoc(*args, **kwargs)	forall x y z, f(f(x,y),z) = f(x,f(y,z))
Asymm(*args, **kwargs)	forall x y, rel(x, y) implies not rel(y, x)
Comm(*args, **kwargs)	forall x y, f(x,y) = f(y,x)
Idem(*args, **kwargs)	forall x, f(x,x) = x
Identity(*args, **kwargs)
Irrefl(*args, **kwargs)	forall x, not rel(x, x)
LeftIdentity(*args, **kwargs)	forall x, f(e,x) = x
Refl(*args, **kwargs)	forall x, rel(x, x)
RightIdentity(*args, **kwargs)	forall x, f(x,e) = x
Total(*args, **kwargs)	forall x y, rel(x, y) or rel(y, x)

class kdrag.property.Antisymm(*args, **kwargs)

Bases: Protocol

forall x y, rel(x, y) and rel(y, x) implies x = y

antisymm: Proof

rel: FuncDeclRef

class kdrag.property.Assoc(*args, **kwargs)

Bases: Protocol

forall x y z, f(f(x,y),z) = f(x,f(y,z))

assoc: Proof

f: FuncDeclRef

class kdrag.property.Asymm(*args, **kwargs)

Bases: Protocol

forall x y, rel(x, y) implies not rel(y, x)

asymm: Proof

rel: FuncDeclRef

class kdrag.property.Comm(*args, **kwargs)

Bases: Protocol

forall x y, f(x,y) = f(y,x)

comm: Proof

f: FuncDeclRef

class kdrag.property.Idem(*args, **kwargs)

Bases: Protocol

forall x, f(x,x) = x

f: FuncDeclRef

idem: Proof

class kdrag.property.Identity(*args, **kwargs)

Bases: LeftIdentity, RightIdentity, Protocol

e: ExprRef

f: FuncDeclRef

left_id: Proof

right_id: Proof

class kdrag.property.Irrefl(*args, **kwargs)

Bases: Protocol

forall x, not rel(x, x)

irrefl: Proof

rel: FuncDeclRef

class kdrag.property.LeftIdentity(*args, **kwargs)

Bases: Protocol

forall x, f(e,x) = x

e: ExprRef

f: FuncDeclRef

left_id: Proof

class kdrag.property.Refl(*args, **kwargs)

Bases: Protocol

forall x, rel(x, x)

refl: Proof

rel: FuncDeclRef

class kdrag.property.RightIdentity(*args, **kwargs)

Bases: Protocol

forall x, f(x,e) = x

e: ExprRef

f: FuncDeclRef

right_id: Proof

class kdrag.property.Total(*args, **kwargs)

Bases: Protocol

forall x y, rel(x, y) or rel(y, x)

rel: FuncDeclRef

total: Proof