natural-number-game

Solututions to the Natural Number Game

NameSizeMode
..
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