{-# OPTIONS --without-K #-} module Explore.BinTree where open import Data.Tree.Binary open import Explore.Core open import Explore.Properties fromBinTree : ∀ {m A} → BinTree A → Explore m A fromBinTree (leaf x) _ _ f = f x fromBinTree (fork ℓ r) ε _∙_ f = fromBinTree ℓ ε _∙_ f ∙ fromBinTree r ε _∙_ f fromBinTree-ind : ∀ {m p A} (t : BinTree A) → ExploreInd p (fromBinTree {m} t) fromBinTree-ind (leaf x) P _ P∙ Pf = Pf x fromBinTree-ind (fork ℓ r) P Pε P∙ Pf = P∙ (fromBinTree-ind ℓ P Pε P∙ Pf) (fromBinTree-ind r P Pε P∙ Pf)