module exampletree1 where

data Bool : Set where
  tt : Bool
  ff : Bool

data ⊥ : Set where

data ⊤ : Set where
  true : ⊤ 


data Tree : Set where
  oak    : Tree
  pine   : Tree
  spruce : Tree


IsConifer : Tree -> Set 
IsConifer oak = ⊥ 
IsConifer _   = ⊤ 


f : ( t : Tree ) -> IsConifer t -> Bool
f pine   _ = {! !}
f spruce _ = {! !}
f oak  ()