kdrag.parsers.microlean.inductive

kdrag.parsers.microlean.inductive(s: str, globals=None) → DatatypeSortRef

Parse an inductive datatype definition.

>>> inductive("inductive boollist where | nil : boollist | cons : Bool -> boollist -> boollist").constructor(0)
nil
>>> Nat = kd.Nat
>>> inductive("inductive foo where | mkfoo : Nat -> foo")
foo

Parameters:

s (str)

Return type:

DatatypeSortRef