kdrag.parsers.microlean.inductive_of_tree

kdrag.parsers.microlean.inductive_of_tree(tree: Tree, globals=None) → DatatypeSortRef

Parse an inductive datatype definition.

>>> tree = inductive_parser.parse("inductive nat where | zero : nat | succ : nat -> nat | fiz : Int -> Bool -> (Bool -> nat) -> nat")
>>> inductive_of_tree(tree).constructor(1)
succ
>>> inductive_of_tree(tree).accessor(1,0)
succ0

Parameters:

tree (Tree)

Return type:

DatatypeSortRef