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