kdrag.theories.univ

Module Attributes

Real0

Type1 = kd.Inductive("Type1") Type1.declare("Type0", ("type0", Type0)) Type1.declare("Seq", ("seq", Type1)) Type1Sort = smt.DatatypeSort("Type1") # We could have deeper recursion at the same universe level # Type1.declare( # "Array", ("array", smt.ArraySort(smt.ArraySort(Type1Sort, Type0), Type1Sort)) # ) Type1.declare("Array", ("array", smt.ArraySort(Type0, Type1Sort))) Type1 = Type1.create()

Functions

`Int`(l)
`Type`(l)	A generic value type at universe level l.

kdrag.theories.univ.Int(l: int) → QuantifierRef

>>> Int(0)
Lambda(x, is(Int, x))
>>> Int(1)
Lambda(x, And(is(Type0, x), is(Int, type0(x))))

Parameters:: l (int)
Return type:: QuantifierRef

kdrag.theories.univ.Real0 = Lambda(x, is(Real, x)): Type1 = kd.Inductive(“Type1”) Type1.declare(“Type0”, (“type0”, Type0)) Type1.declare(“Seq”, (“seq”, Type1)) Type1Sort = smt.DatatypeSort(“Type1”) # We could have deeper recursion at the same universe level # Type1.declare( # “Array”, (“array”, smt.ArraySort(smt.ArraySort(Type1Sort, Type0), Type1Sort)) # ) Type1.declare(“Array”, (“array”, smt.ArraySort(Type0, Type1Sort))) Type1 = Type1.create()

kdrag.theories.univ.Type(l: int) → DatatypeSortRef

A generic value type at universe level l. >>> Type(1) Type1

Parameters:: l (int)
Return type:: DatatypeSortRef