kdrag.datatype.InductiveRel

kdrag.datatype.InductiveRel(name: str, *params: ExprRef) → Datatype

Define an inductive type of evidence and a relation the recurses on that evidence

>>> x = smt.Int("x")
>>> Even = InductiveRel("Even", x)
>>> Even.declare("Ev_Z",                           pred = x == 0)
>>> Even.declare("Ev_SS", ("sub2_evidence", Even), pred = lambda evid: evid.rel(x-2))
>>> Even = Even.create()
>>> smt.Const("ev", Even).rel(4)
even(ev, 4)

Parameters:

name (str)
params (ExprRef)

Return type:

Datatype