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()
>>> ev = smt.Const("ev", Even)
>>> ev.rel(4)
even(4)[ev]
>>> ev(4)
even(4)[ev]
>>> Even(4)
even(4)

Parameters:

name (str)
params (ExprRef)

Return type:

Datatype