kdrag.printers.lean.of_datatype

kdrag.printers.lean.of_datatype(dt: DatatypeSortRef) → str

Convert a datatype to a Lean inductive type definition.

>>> Nat = smt.Datatype("Nat")
>>> Nat.declare("Zero")
>>> Nat.declare("Succ", ("pred", Nat))
>>> Nat = Nat.create()
>>> of_datatype(Nat)
'inductive Nat : Type where\n| Zero : Nat\n| Succ : Nat -> Nat\nderiving BEq, Inhabited, Repr, DecidableEq\n'

Parameters:

dt (DatatypeSortRef)

Return type:

str