From d9ddffd55ed97b1b9a7c1fa3e4ca46126455e411 Mon Sep 17 00:00:00 2001
From: wadler <wadler@inf.ed.ac.uk>
Date: Wed, 16 May 2018 12:47:04 -0300
Subject: [PATCH] created Head to ask for help

---
 src/extra/Head.agda | 40 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 40 insertions(+)
 create mode 100644 src/extra/Head.agda

diff --git a/src/extra/Head.agda b/src/extra/Head.agda
new file mode 100644
index 00000000..53639a4f
--- /dev/null
+++ b/src/extra/Head.agda
@@ -0,0 +1,40 @@
+import Relation.Binary.PropositionalEquality as Eq
+open Eq using (_≡_; refl; sym; trans; cong; cong₂; _≢_)
+open import Data.Empty using (⊥; ⊥-elim)
+open import Data.List using (List; []; _∷_; dropWhile)
+open import Data.Char using (Char)
+open import Data.Bool using (Bool; true; false)
+import Data.Char as Char using (_≟_)
+open import Relation.Nullary using (¬_; Dec; yes; no)
+open import Relation.Nullary.Decidable using (⌊_⌋)
+
+
+data Head {A : Set} (P : A → Bool) : List A → Set where
+  head : ∀ (c : A) (s : List A) → P c ≡ true → Head P (c ∷ s)
+
+prime : Char
+prime = '′'
+
+isPrime : Char → Bool
+isPrime c = ⌊ c Char.≟ prime ⌋
+
+head-lemma : ∀ (s : List Char) → ¬ Head isPrime (dropWhile isPrime s)
+head-lemma [] = λ()
+head-lemma (c ∷ s) with isPrime c 
+...                   | true       =  head-lemma s
+...                   | false      =  ¬h
+  where
+  ¬h : ¬ Head isPrime (c ∷ s)
+  ¬h (head c s eqn′) = {!!}
+
+{-
+Goal: ⊥
+————————————————————————————————————————————————————————————
+s    : List Char
+c    : Char
+eqn′ : ⌊ (c Char.≟ '′' | .Agda.Builtin.Char.primCharEquality c '′')
+       ⌋
+       ≡ true
+s    : List Char
+c    : Char
+-}