draft

fbt.agda

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)
open import Data.Nat
open import Data.Bool.Base


data Tree : Set where
  tempty  : Tree
  tnode   : ℕ -> Tree -> Tree -> Tree

sum-tree : Tree -> ℕ
sum-tree tempty = 0
sum-tree (tnode n l r) = n + sum-tree l + sum-tree r

_ : sum-tree (tnode 5 (tnode 4 tempty tempty) tempty) ≡ 9
_ = refl

max : ℕ -> ℕ -> ℕ
max zero b = b
max a zero = a
max (suc a) (suc b) = suc (max a b)

max-tree : Tree -> ℕ
max-tree tempty = 0
max-tree (tnode n tempty tempty) = n
max-tree (tnode n l r) = max n (max (max-tree l) (max-tree r))

_ : max-tree (tnode 5 (tnode 4 (tnode 5 (tnode 4 tempty tempty) tempty) tempty)
                      (tnode 2 (tnode 6 (tnode 4 tempty tempty) tempty) tempty)) ≡ 6
_ = refl

in-tree : Tree -> ℕ -> Bool
in-tree tempty _ = false
in-tree (tnode this l r) q with compare this q
... | Data.Nat.equal _ = true
... | _ = (in-tree l q) ∨ (in-tree r q)

_ : in-tree (tnode 5 (tnode 4 (tnode 5 (tnode 4 tempty tempty) tempty) tempty)
                     (tnode 2 (tnode 6 (tnode 4 tempty tempty) tempty) tempty))
            2 ≡ true
_ = refl