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
>>> nat = inductive("inductive nat where | zero : nat | succ : nat -> nat | fiz : Int -> Bool -> (Bool -> nat) -> nat")
>>> nat.constructor(1)
succ
>>> nat.accessor(1,0)
succ0

Parameters:

s (str)

Return type:

DatatypeSortRef