Где я могу найти определения бинарных деревьев и алгоритмы, связанные с ними в Изабель?

Question

Где я могу найти определение бинарного дерева и алгоритмы, связанные с бинарными деревьями в Изабель?

Я новичок в Изабель и поэтому ищу новые учебные материалы.Недавно я пытался найти определение бинарного дерева и алгоритмы на бинарных деревьях в Изабель, но, к сожалению, моя попытка не удалась.Где я могу их найти?Заранее благодарю за помощь.

Answer 1

Двоичные деревья определены в библиотеке HOL (~~/src/HOL/Library/Tree.thy).Некоторые алгоритмы для них (т.е. реализации структур данных, таких как деревья AVL с ними) определены в HOL-Data_Structures (~~/src/HOL/Data_Structures/).

Оба из них находятся в распределении Изабель.Вы можете импортировать их, написав, например, "Data_Structures.AVL_Set" или "HOL-Library.Tree" (кавычки требуются, если в имени есть тире).