1
module CoverStrategy where
4
open import Common.Prelude renaming (Nat to ℕ)
6
data _∼_ : ℕ → ℕ → Set where
10
max : ∀ {m n} → m ∼ n → ℕ
14
data Tree : ℕ → Set where
15
node : ∀ {hˡ hʳ} (bal : hˡ ∼ hʳ) → Tree (max bal)
17
test : ∀ {hˡ hʳ} → Tree hˡ → hˡ ∼ hʳ → Set
22
{- We cannot split on 'Tree hˡ' if we have already split on 'hˡ ∼ hʳ'
23
bla : ∀ {hˡ hʳ} → Tree hˡ → hˡ ∼ hʳ → Set