[Agda] isHead x (x :: xs)

Sergei Meshveliani mechvel at botik.ru
Fri May 17 10:57:09 CEST 2013


Please, how to prove the following?

  isHead : ℕ → List ℕ → Bool
  isHead _ []        = false 
  isHead x (y ∷ ys)  with  x ≟ y
  ...              | yes _ = true 
  ...              | no _  = false 

  isHP : (x : ℕ) → (xs : List ℕ) → isHead x (x ∷ xs) ≡ true
  isHP x xs =
              ??

Thanks,

------
Sergei



More information about the Agda mailing list