kdrag.theories.univ

Module Attributes

Bool	S = smt.Const("S", smt.SetSort(Type)) mul = smt.Const("mul", smt.ArraySort(Type, Type, Type)) semigroup = kd.define( "semigroup", [S, mul], smt.And(kd.Closed(S, mul), kd.Assoc(mul, T=S)) )

Functions

box(term)
cast(s, term)
poly_ax(s)

kdrag.theories.univ.Bool = Lambda(x, is(Bool, x))

S = smt.Const(“S”, smt.SetSort(Type)) mul = smt.Const(“mul”, smt.ArraySort(Type, Type, Type)) semigroup = kd.define(

“semigroup”, [S, mul], smt.And(kd.Closed(S, mul), kd.Assoc(mul, T=S))

)

kdrag.theories.univ.box(term: ExprRef) → ExprRef

Parameters:

term (ExprRef)

Return type:

ExprRef

kdrag.theories.univ.cast(s: SortRef, term: ExprRef) → ExprRef

Parameters:

• s (SortRef)

• term (ExprRef)

Return type:

ExprRef

kdrag.theories.univ.poly_ax(s: SortRef) → Proof

>>> kd.prove(cast(smt.IntSort(), box(smt.IntVal(42))) == 42, by=[poly_ax(smt.IntSort())])
|= cast_Int(box(42)) == 42

Parameters:

s (SortRef)

Return type:

Proof