natural-number-game
Solututions to the Natural Number Game
Name | Size | Mode | |
.. | |||
function.lean | 1525B | -rw-r--r-- |
01 02 03 04 05 06 07 08 09 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86
example (P Q : Type) (p : P) (h : P → Q) : Q := begin exact h(p), end example : ℕ → ℕ := begin intro n, exact 3 * n + 2, end example (P Q R S T U: Type) (p : P) (h : P → Q) (i : Q → R) (j : Q → T) (k : S → T) (l : T → U) : U := begin have q := h(p), have t := j(q), exact l(t), end example (P Q R S T U: Type) (p : P) (h : P → Q) (i : Q → R) (j : Q → T) (k : S → T) (l : T → U) : U := begin have q := h(p), have t := j(q), exact l(t), end example (P Q : Type) : P → (Q → P) := begin intros p q, exact p, end example (P Q R : Type) : (P → (Q → R)) → ((P → Q) → (P → R)) := begin intros f g p, apply f, exact p, apply g, exact p, end example (P Q F : Type) : (P → Q) → ((Q → F) → (P → F)) := begin intros f g p, apply g, apply f, exact p, end example (P Q F : Type) : (P → Q) → ((Q → F) → (P → F)) := begin intros f g p, apply g, apply f, exact p, end example (A B C D E F G H I J K L : Type) ( f1 : A → B) ( f2 : B → E) ( f3 : E → D) ( f4 : D → A) ( f5 : E → F) ( f6 : F → C) ( f7 : B → C) ( f8 : F → G) ( f9 : G → J) (f10 : I → J) (f11 : J → I) (f12 : I → H) (f13 : E → H) (f14 : H → K) (f15 : I → L) : A → L := begin intro a, apply f15, apply f11, apply f9, apply f8, apply f5, apply f2, apply f1, exact a, end