Существуют ли какие-либо предопределенные функции для бинарных деревьев в Изабель? Например, чтобы перейти к левой стороне двоичного дерева?Предопределенные функции для двоичных деревьев в Isabelle
0
A
ответ
1
С Isabelle2014 существует небольшая теория для двоичных деревьев в ~~/src/HOL/Library/Tree
. Если этот тип соответствует вашей цели, вы можете использовать его и функции, определенные на нем. Например, существуют селекторные функции left
и right
, которые возвращают левое и правое поддерево дерева.
Если вам нужно определить свой собственный тип данных, вы можете использовать синтаксис селектора datatype_new
для определения селекторов по своему усмотрению.