Created
July 16, 2018 10:47
-
-
Save lthms/9f3e3d0b8d71da4ebc7e77db174d1c85 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
inductive seq (α: Type) : Type | |
| cons : α -> seq -> seq | |
| nil {} : seq | |
open seq | |
def apply {α β} (f: α -> β) : seq α -> seq β | |
| nil := nil | |
| (cons x rst) := cons (f x) (apply rst) | |
theorem apply_singleton {α β} : | |
forall (f: α -> β) (x: α), | |
apply f (cons x nil) = cons (f x) nil := | |
begin | |
intros, | |
refl, | |
end | |
def size {α: Type} : seq α -> nat | |
| nil := 0 | |
| (cons _ rst) := size rst + 1 | |
def head {α} (l: seq α) : (0 < size l) -> α := | |
begin | |
intro H, | |
induction l with x rst, | |
case seq.cons { exact x }, | |
case seq.nil { unfold size at H, exfalso, cases H } | |
end |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment