Редактирование: Я обнаружил, что если я встраиваю определение t1 напрямую, этот тип проверяется просто отлично. Таким образом, кажется, что определение обрабатывает t1 как только неизвестную переменную, а не как мое фактическое более раннее определение. Есть ли способ заставить это?Функция проверки оценивается как True в Idris
Предисловие: Я полностью понимаю, что это не идиоматический способ написать это. Я просто хочу понять, что здесь происходит конкретно.
Я написал тривиальное реализацию бинарного дерева и функции elemBT которая проверяет, содержит ли дерево конкретный элемент и оценивающего к Boolean (думаю elem функции в Haskell, для бинарных деревьев, за исключением).
t1 : BT Nat
t1 = Node 5 Nil Nil
elemBT : Eq a => a -> BT a -> Bool
> elemBT 5 t1
True : Bool
Теперь, когда я знаю, что elemBT оценивает в True, я ожидаю, чтобы иметь возможность написать очень простое заявление, которое доказывает, что, выполнив следующие действия.
t1contains5 : elemBT 5 t1 = True
t1contains5 = Refl
Неожиданно это приводит к сбою объединения. Тем не менее, я могу сделать почти то же самое, используя встроенные списки.
junk : elem 5 [1,5] = True
junk = Refl
И этот тип проверяет как ожидалось. Почему мой пример с бинарными деревьями работает одинаково?
Спасибо.